Relating Syntactic and Semantic Perturbations of Hybrid Automata
We investigate how the semantics of a hybrid automaton deviates with respect to syntactic perturbations on the hybrid automaton. We consider syntactic perturbations of a hybrid automaton, wherein the syntactic representations of its elements, namely, initial sets, invariants, guards, and flows, in some logic are perturbed. Our main result establishes a continuity like property that states that small perturbations in the syntax lead to small perturbations in the semantics. More precisely, we show that for every real number epsilon>0 and natural number k, there is a real number delta>0 such that H^delta, the delta syntactic perturbation of a hybrid automaton H, is epsilon-simulation equivalent to H up to k transition steps. As a byproduct, we obtain a proof that a bounded safety verification tool such as dReach will eventually prove the safety of a safe hybrid automaton design (when only non-strict inequalities are used in all constraints) if dReach iteratively reduces the syntactic parameter delta that is used in checking approximate satisfiability. This has an immediate application in counter-example validation in a CEGAR framework, namely, when a counter-example is spurious, then we have a complete procedure for deducing the same.
Model Checking
Hybrid Automata
Approximation
Perturbation
Computer systems organization~Embedded and cyber-physical systems
Theory of computation~Timed and hybrid models
Software and its engineering~Model checking
26:1-26:16
Regular Paper
Mahesh Viswanathan was partially supported by NSF CSR 1422798, and Pavithra Prabhakar was partially supported by NSF CAREER Award No. 1552668 and ONR YIP Award No. N00014-17-1-257.
Nima
Roohi
Nima Roohi
Univeristy of Pennsylvania, USA
Pavithra
Prabhakar
Pavithra Prabhakar
Kansas State University, USA, http://people.cs.ksu.edu/~pprabhakar/
Mahesh
Viswanathan
Mahesh Viswanathan
University of Illinois at Urbana-Champaign, USA, http://vmahesh.cs.illinois.edu/
10.4230/LIPIcs.CONCUR.2018.26
E. Asarin and A. Bouajjani. Perturbed turing machines and hybrid systems. In LICS, pages 269-278, 2001.
R.G. Bartle and D.R. Sherbert. Introduction to Real Analysis, 4th Edition. John Wiley &Sons, Incorporated, 2011.
P. Bouyer, N. Markey, and P.-A. Reynier. Robust model-checking of linear-time properties in timed automata. In Proceedings of LATIN, pages 238-249, 2006.
Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust model-checking of timed automata via pumping in channel machines. In Proceedings of FORMATS, pages 97-112, 2011.
Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, 2007.
Vasco Brattka, Peter Hertling, and Klaus Weihrauch. A Tutorial on Computable Analysis, pages 425-491. Springer New York, New York, NY, 2008.
Martin de Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robust safety of timed automata. Formal Methods in System Design, 33(1):45-84, 2008.
Peter Franek, Stefan Ratschan, and Piotr Zgliczynski. Quasi-decidability of a fragment of the first-order theory of real numbers. Journal of Automated Reasoning, 57(2):157-185, Aug 2016.
Martin Fränzle. Analysis of Hybrid Systems: An Ounce of Realism Can Save an Infinity of States, pages 126-139. Springer Berlin Heidelberg, Berlin, Heidelberg, 1999.
Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. δ-completee decision procedures for satisfiability over the reals. In IJCAR, pages 286-300, Berlin, Heidelberg, 2012. Springer-Verlag.
Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. Delta-decidability over the reals. In LICS, pages 305-314. IEEE Computer Society, 2012.
Sicun Gao, Soonho Kong, Wei Chen, and Edmund M. Clarke. Delta-complete analysis for bounded reachability of hybrid systems. CoRR, abs/1404.7171, 2014.
Antoine Girard. Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pages 824-829, 2014.
Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan. Robust timed automata, pages 331-345. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997.
Thomas A. Henzinger and Jean-François Raskin. Robust Undecidability of Timed and Hybrid Systems, pages 145-159. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000.
K.I. Ko. Complexity theory of real functions. Progress in theoretical computer science. Birkhäuser, 1991.
Ruggero Lanotte and Simone Tini. Taylor approximation for hybrid systems. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, pages 402-416, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
Ruggero Lanotte and Simone Tini. Taylor approximation for hybrid systems. Information and Computation, 205(11):1575-1607, 2007.
M. O'Searcoid. Metric Spaces. Springer Undergraduate Mathematics Series. Springer London, 2006.
Giordano Pola, Antoine Girard, and Paulo Tabuada. Approximately bisimilar symbolic models for nonlinear control systems. Automatica, 44(10):2508-2516, 2008.
Pavithra Prabhakar and Mahesh Viswanathan. A dynamic algorithm for approximate flow computations. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 133-142, 2011.
Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, and Geir E. Dullerud. Verifying tolerant systems using polynomial approximations. In Proceedings of the 30th IEEE Real-Time Systems Symposium, RTSS 2009, Washington, DC, USA, 1-4 December 2009, pages 181-190, 2009.
Anuj Puri. Dynamical properties of timed automata. Discrete Event Dynamic Systems, 10(1-2):87-113, 2000.
Stefan Ratschan. Quantified constraints under perturbation. Journal of Symbolic Computation, 33(4):493-505, 2002.
Stefan Ratschan. Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Logic, 7(4):723-748, 2006.
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata, pages 573-588. Springer, 2017.
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Robust model checking of timed automata under clock drifts. In HSCC, pages 153-162. ACM, 2017.
K. Weihrauch. Computable Analysis: An Introduction. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin Heidelberg, 2000.
M. De Wulf, L. Doyen, N. Markey, and J.-F. Raskin. Robustness and implementability of timed automata. In Proceedings of FORMATS, pages 118-133, 2004.
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode