Document Open Access Logo

Relating Syntactic and Semantic Perturbations of Hybrid Automata

Authors Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.26.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Nima Roohi
  • Univeristy of Pennsylvania, USA
Pavithra Prabhakar
  • Kansas State University, USA, http://people.cs.ksu.edu/~pprabhakar/
Mahesh Viswanathan
  • University of Illinois at Urbana-Champaign, USA, http://vmahesh.cs.illinois.edu/

Funding

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.

Cite As Get BibTex

Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Relating Syntactic and Semantic Perturbations of Hybrid Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.26

Abstract

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.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Embedded and cyber-physical systems
  • Theory of computation → Timed and hybrid models
  • Software and its engineering → Model checking
Keywords
  • Model Checking
  • Hybrid Automata
  • Approximation
  • Perturbation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. E. Asarin and A. Bouajjani. Perturbed turing machines and hybrid systems. In LICS, pages 269-278, 2001. Google Scholar
  2. R.G. Bartle and D.R. Sherbert. Introduction to Real Analysis, 4th Edition. John Wiley &Sons, Incorporated, 2011. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, 2007. Google Scholar
  6. Vasco Brattka, Peter Hertling, and Klaus Weihrauch. A Tutorial on Computable Analysis, pages 425-491. Springer New York, New York, NY, 2008. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. Delta-decidability over the reals. In LICS, pages 305-314. IEEE Computer Society, 2012. Google Scholar
  12. Sicun Gao, Soonho Kong, Wei Chen, and Edmund M. Clarke. Delta-complete analysis for bounded reachability of hybrid systems. CoRR, abs/1404.7171, 2014. Google Scholar
  13. 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. Google Scholar
  14. Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan. Robust timed automata, pages 331-345. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. Google Scholar
  15. Thomas A. Henzinger and Jean-François Raskin. Robust Undecidability of Timed and Hybrid Systems, pages 145-159. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. Google Scholar
  16. K.I. Ko. Complexity theory of real functions. Progress in theoretical computer science. Birkhäuser, 1991. Google Scholar
  17. 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. Google Scholar
  18. Ruggero Lanotte and Simone Tini. Taylor approximation for hybrid systems. Information and Computation, 205(11):1575-1607, 2007. Google Scholar
  19. M. O'Searcoid. Metric Spaces. Springer Undergraduate Mathematics Series. Springer London, 2006. Google Scholar
  20. Giordano Pola, Antoine Girard, and Paulo Tabuada. Approximately bisimilar symbolic models for nonlinear control systems. Automatica, 44(10):2508-2516, 2008. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. Anuj Puri. Dynamical properties of timed automata. Discrete Event Dynamic Systems, 10(1-2):87-113, 2000. Google Scholar
  24. Stefan Ratschan. Quantified constraints under perturbation. Journal of Symbolic Computation, 33(4):493-505, 2002. Google Scholar
  25. Stefan Ratschan. Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Logic, 7(4):723-748, 2006. Google Scholar
  26. Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata, pages 573-588. Springer, 2017. Google Scholar
  27. Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Robust model checking of timed automata under clock drifts. In HSCC, pages 153-162. ACM, 2017. Google Scholar
  28. K. Weihrauch. Computable Analysis: An Introduction. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin Heidelberg, 2000. Google Scholar
  29. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact