Automatic time-unbounded reachability analysis of hybrid systems (Record no. 430276)

000 -LEADER
fixed length control field 03073ntm a22003497a 4500
003 - CONTROL NUMBER IDENTIFIER
control field AT-ISTA
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20200722172852.0
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 200722s2019 au ||||| m||| 00| 0 eng d
040 ## - CATALOGING SOURCE
Transcribing agency IST
100 ## - MAIN ENTRY--PERSONAL NAME
Personal name Giacobbe, Mirco
9 (RLIN) 215074
245 ## - TITLE STATEMENT
Title Automatic time-unbounded reachability analysis of hybrid systems
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Name of publisher, distributor, etc. IST Austria
Date of publication, distribution, etc. 2019
500 ## - GENERAL NOTE
General note Thesis
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note Abstract
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note Acknowledgments
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note About the Author
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Publications
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Tables
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Figures
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Abbreviations
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 1. Introduction
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 2. Template-polyhedral Abstraction of Hybrid Automata
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 3. Automatic Template Refinement
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 4. Counterexample-guided Refinement for Convex Hybrid Automata
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 5. Conic Abstractions for Affine Hybrid Automata
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 6. Space-Time Interpolation for Affine Hybrid Automata
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 7. Conclusions
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note Bibliography
520 ## - SUMMARY, ETC.
Summary, etc. Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving. Nevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions. While, previously, directions were given by the user, we introduce (1) the first method for computing template directions from spurious counterexamples, so as to generalize and eliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid automata with (possibly non-linear) convex constraints on derivatives only, while for linear ODE requires further abstraction. Specifically, we introduce (2) the conic abstractions, which, partitioning the state space into appropriate (possibly non-uniform) cones, divide curvy trajectories into relatively straight sections, suitable for polyhedral abstractions. Finally, we introduce (3) space-time interpolation, which, combining interval arithmetic and template refinement, computes appropriate (possibly non-uniform) time partitioning and template directions along spurious trajectories, so as to eliminate them. We obtain sound and automatic methods for the reachability analysis over dense and unbounded time of convex hybrid automata and hybrid automata with linear ODE. We build prototype tools and compare—favorably—our methods against the respective state-of-the-art tools, on several benchmarks.
856 ## - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://doi.org/10.15479/AT:ISTA:6894">https://doi.org/10.15479/AT:ISTA:6894</a>
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Source of classification or shelving scheme
Holdings
Withdrawn status Lost status Source of classification or shelving scheme Damaged status Not for loan Permanent Location Current Location Date acquired Barcode Date last seen Price effective from Koha item type
  Not Lost       Library Library 2020-07-22 AT-ISTA#002086 2020-07-22 2020-07-22 Book

Powered by Koha