Document Open Access Logo

Finite Bisimulations for Dynamical Systems with Overlapping Trajectories

Authors Béatrice Bérard, Patricia Bouyer, Vincent Jugé

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2018.26.pdf
  • Filesize: 494 kB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Reachability properties
  • dynamical systems
  • o-minimal structures
  • intersecting trajectories
  • finite bisimulations

Metrics

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

Abstract

Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.

Cite As Get BibTex

Béatrice Bérard, Patricia Bouyer, and Vincent Jugé. Finite Bisimulations for Dynamical Systems with Overlapping Trajectories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.26

Author Details

Béatrice Bérard
  • Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, F-75005 Paris, France
Patricia Bouyer
  • LSV, CNRS, ENS Paris-Saclay, Univ. Paris-Saclay, France
Vincent Jugé
  • Université Paris-Est, LIGM (UMR 8049), CNRS, ENPC, ESIEE, UPEM, F-77454, Marne-la-Vallée, France

Funding

  • Bouyer, Patricia: Supported by ERC project EQualIS.

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  2. Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, and George J. Pappas. Discrete abstractions of hybrid systems. Proc. of the IEEE, 88:971-984, 2000. Google Scholar
  3. Béatrice Bérard, Serge Haddad, Claudine Picaronny, Mohab Safey El Din, and Mathieu Sassolas. Polynomial Interrupt Timed Automata. In Proceedings of the 9th International Workshop on Reachability problems (RP'15), volume 9328 of LNCS, pages 20-32. Springer, 2015. Google Scholar
  4. Thomas Brihaye. A note on the undecidability of the reachability problem for o-minimal dynamical systems. Math. Log. Q., 52(2):165-170, 2006. URL: http://dx.doi.org/10.1002/malq.200510024.
  5. Thomas Brihaye. Verification and Control of O-Minimal Hybrid Systems and Weighted Timed Automata. PhD thesis, Université de Mons-Hainaut, Belgium, 2006. Google Scholar
  6. Thomas Brihaye. Words and bisimulation of dynamical systems. Discrete Mathematics and Theoretical Computer Science, 9(2):11-31, 2007. Google Scholar
  7. Thomas Brihaye and Christian Michaux. On the expressiveness and decidability of o-minimal hybrid systems. Journal of Complexity, 21(4):447-478, 2005. Google Scholar
  8. Thomas Brihaye, Christian Michaux, Cédric Rivière, and Christophe Troestler. On o-minimal hybrid systems. In Proc. 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04), volume 2993 of Lecture Notes in Computer Science, pages 219-233. Springer, 2004. Google Scholar
  9. Alberto Casagrande, Pietro Corvaja, Carla Piazza, and Bud Mishra. Decidable compositions of o-minimal automata. In Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan, editors, Proc. of 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008, volume 5311 of Lecture Notes in Computer Science, pages 274-288. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-88387-6_25.
  10. Alberto Casagrande, Carla Piazza, Alberto Policriti, and Bud Mishra. Inclusion dynamics hybrid automata. Inf. Comput., 206(12):1394-1424, 2008. URL: http://dx.doi.org/10.1016/j.ic.2008.09.001.
  11. Gregory J Chaitin. A theory of program size formally identical to information theory. Journal of the ACM (JACM), 22(3):329-340, 1975. Google Scholar
  12. Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. Taylor model flowpipe construction for non-linear hybrid systems. In Proceedings of the 33rd IEEE Real-Time Systems Symposium, RTSS 2012, pages 183-192. IEEE Computer Society, 2012. URL: http://dx.doi.org/10.1109/RTSS.2012.70.
  13. G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages 2nd GI Conference, volume 33 of Lecture Notes in Computer Science, pages 134-183. Springer, 1975. Google Scholar
  14. Jennifer M. Davoren. Topologies, continuity and bisimulations. Informatique Théorique et Applications, 33(4-5):357-382, 1999. Google Scholar
  15. Raffaella Gentilini. Reachability problems on extended o-minimal hybrid automata. In Proc. 3rd International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'05), volume 3829 of Lecture Notes in Computer Science, pages 162-176. Springer, 2005. Google Scholar
  16. R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Hybrid systems, volume 736 of LNCS. Springer, 1993. Google Scholar
  17. Emmanuel Hainry. Reachability in linear dynamical systems. In Logics and Theory of Algorithms, Proc. 4th Conference on Computability in Europe (CiE'08), volume 5028 of Lecture Notes in Computer Science, pages 241-250. Springer, 2008. Google Scholar
  18. Thomas A. Henzinger. Hybrid automata with finite bisimulations. In Proc. 22nd International Colloquium on Automata, Languages and Programming (ICALP'95), volume 944 of Lecture Notes in Computer Science, pages 324-335. Springer, 1995. Google Scholar
  19. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94-124, 1998. Google Scholar
  20. Wilfrid Hodges. A Shorter Model Theory. Cambridge University Press, 1997. Google Scholar
  21. Julia F. Knight, Anand Pillay, and Charles Steinhorn. Definable sets in ordered structures. II. Transactions of the American Mathematical Society, 295(2):593-605, 1986. Google Scholar
  22. Margarita V. Korovina and Nicolai Vorobjov. Upper and lower bounds on sizes of finite bisimulations of Pfaffian hybrid systems. In CiE, volume 3988 of Lecture Notes in Computer Science, pages 267-276. Springer, 2006. Google Scholar
  23. Gerardo Lafferriere, George J. Pappas, and Shankar Sastry. Hybrid systems with finite bisimulations. In Proc. Hybrid Systems V: Verification and Control (1997), volume 1567 of Lecture Notes in Computer Science, pages 186-203. Springer, 1997. Google Scholar
  24. Gerardo Lafferriere, George J. Pappas, and Shankar Sastry. Subanalytic stratifications and bisimulations. In Proc. 1st International Workshop on Hybrid Systems: Computation and Control (HSCC'98), volume 1386 of Lecture Notes in Computer Science, pages 205-220. Springer, 1998. Google Scholar
  25. Gerardo Lafferriere, George J. Pappas, and Shankar Sastry. O-minimal hybrid systems. Mathematics of Control, Signals, and Systems, 13(1):1-21, 2000. Google Scholar
  26. Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. A new class of decidable hybrid systems. In Proc. 2nd International Workshop on Hybrid Systems: Computation and Control (HSCC'99), volume 1569 of Lecture Notes in Computer Science, pages 137-151. Springer, 1999. Google Scholar
  27. Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Kreiseliana, pages 441-467. A. K. Peters, 1996. Google Scholar
  28. David Marker. Model theory: an introduction, volume 217. Springer Science &Business Media, 2006. Google Scholar
  29. Daniel J Miller. Constructing o-minimal structures with decidable theories using generic families of functions from quasianalytic classes. Research Report math.LO/1008.2575, arXiv, 2010. Google Scholar
  30. Anand Pillay and Charles Steinhorn. Definable sets in ordered structures. Bulletin of the American Mathematical Society, 11(1), 1984. Google Scholar
  31. Anand Pillay and Charles Steinhorn. Definable sets in ordered structures. I. Transactions of the American Mathematical Society, 295(2):565-592, 1986. Google Scholar
  32. Anand Pillay and Charles Steinhorn. Discrete o-minimal structures. Ann. Pure Appl. Logic, 34(3):275-289, 1987. URL: http://dx.doi.org/10.1016/0168-0072(87)90004-2.
  33. Anand Pillay and Charles Steinhorn. Definable sets in ordered structures. III. Transactions of the American Mathematical Society, 309(2):469-476, 1988. Google Scholar
  34. Ashish Tiwari and Gaurav Khanna. Series of abstractions for hybrid automata. In C. J. Tomlin and M. R. Greenstreet, editors, Hybrid Systems: Computation and Control HSCC, volume 2289 of LNCS, pages 465-478. Springer, 2002. Google Scholar
  35. Lou van den Dries. O-minimal structures. In Proc. Logic, From Foundations to Applications, pages 137-185. Oxford University Press, 1996. Google Scholar
  36. Lou van den Dries. Tame Topology and O-Minimal Structures, volume 248 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1998. Google Scholar
  37. Alex J. Wilkie. Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. Journal of the AMS, 9(4):1051-1094, 1996. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact