Formal language properties of hybrid systems with strong resets

Thomas Brihaye; Véronique Bruyère; Elaine Render

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 44, Issue: 1, page 79-111
  • ISSN: 0988-3754

Abstract

top
We study hybrid systems with strong resets from the perspective of formal language theory. We define a notion of hybrid regular expression and prove a Kleene-like theorem for hybrid systems. We also prove the closure of these systems under determinisation and complementation. Finally, we prove that the reachability problem is undecidable for synchronized products of hybrid systems.

How to cite

top

Brihaye, Thomas, Bruyère, Véronique, and Render, Elaine. "Formal language properties of hybrid systems with strong resets." RAIRO - Theoretical Informatics and Applications 44.1 (2010): 79-111. <http://eudml.org/doc/250694>.

@article{Brihaye2010,
abstract = { We study hybrid systems with strong resets from the perspective of formal language theory. We define a notion of hybrid regular expression and prove a Kleene-like theorem for hybrid systems. We also prove the closure of these systems under determinisation and complementation. Finally, we prove that the reachability problem is undecidable for synchronized products of hybrid systems. },
author = {Brihaye, Thomas, Bruyère, Véronique, Render, Elaine},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Hybrid systems with strong resets; formal language theory.; hybrid systems with strong resets; formal language theory},
language = {eng},
month = {2},
number = {1},
pages = {79-111},
publisher = {EDP Sciences},
title = {Formal language properties of hybrid systems with strong resets},
url = {http://eudml.org/doc/250694},
volume = {44},
year = {2010},
}

TY - JOUR
AU - Brihaye, Thomas
AU - Bruyère, Véronique
AU - Render, Elaine
TI - Formal language properties of hybrid systems with strong resets
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/2//
PB - EDP Sciences
VL - 44
IS - 1
SP - 79
EP - 111
AB - We study hybrid systems with strong resets from the perspective of formal language theory. We define a notion of hybrid regular expression and prove a Kleene-like theorem for hybrid systems. We also prove the closure of these systems under determinisation and complementation. Finally, we prove that the reachability problem is undecidable for synchronized products of hybrid systems.
LA - eng
KW - Hybrid systems with strong resets; formal language theory.; hybrid systems with strong resets; formal language theory
UR - http://eudml.org/doc/250694
ER -

References

top
  1. R. Alur and D. Dill, Automata for modeling real-time systems. In ICALP'90: Automata, Languages, and Programming. Lect. Notes Comput. Sci.443 (1990) 322–335.  Zbl0765.68150
  2. R. Alur and D. Dill, A theory of timed automata. Theoret. Comput. Sci.126 (1994) 183–235.  Zbl0803.68071
  3. R. Alur and P. Madhusudan, Decision problems for timed automata: A survey. In SFM'04: School on Formal Methods. Lect. Notes Computer Sci.3185 (2004) 1–24.  Zbl1105.68057
  4. R. Alur, C. Courcoubetis and D.L. Dill, Model-checking in dense real-time. Inform. Comput.104 (1993) 2–34.  Zbl0783.68076
  5. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine, The algorithmic analysis of hybrid systems. Theoret. Comput. Sci.138 (1995) 3–34.  Zbl0823.68067
  6. R. Alur, L. Fix and T.A. Henzinger, Event-clock automata: a determinizable class of timed automata. Theoret. Comput. Sci.211 (1999) 253–273.  Zbl0912.68132
  7. R. Alur, S. La Torre and G.J. Pappas, Optimal paths in weighted timed automata. In HSCC'01: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.203 (2001) 449–62.  Zbl0991.93076
  8. E. Asarin, P. Caspi and O. Maler, A kleene theorem for timed automata. In LICS (1997) 160–171.  
  9. D. Beauquier, Pumping lemmas for timed automata. In Foundations of software science and computation structures (Lisbon, 1998). Lect. Notes Comput. Sci.1378 (1998) 81–94.  Zbl0902.68129
  10. G. Behrmann, A. Fehnker, T. Hune, K.G. Larsen, P. Pettersson, J. Romijn and F. Vaandrager, Minimum-cost reachability for priced timed automata. In HSCC'01: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.2034 (2001) 147–161.  Zbl0991.68037
  11. B. Bérard, A. Petit, V. Diekert and P. Gastin, Characterization of the expressive power of silent transitions in timed automata. Fund. Inform.36 (1998) 145–182.  Zbl0930.68077
  12. P. Bouyer and A. Petit, A Kleene/büchi-like theorem for clock languages. J. Autom. Lang. Comb.7 (2002) 167–186.  Zbl1031.68121
  13. P. Bouyer, T. Brihaye and F. Chevalier, Control in o-minimal hybrid systems. In LICS'06: Logic Comput. Sci. 367–378. IEEE Computer Society Press (2006).  
  14. P. Bouyer, T. Brihaye and F. Chevalier, Weighted o-minimal hybrid systems are more decidable than weighted timed automata! In LFCS'07: Logical Foundations of Computer Science. Lect. Notes Comput. Sci.4514 (2007) 69–83.  Zbl1132.68466
  15. P. Bouyer, S. Haddad and P.-A. Reynier, Undecidability results for timed automata with silent transitions. Research Report LSV-07-12, Laboratoire Spécification et Vérification, ENS Cachan, France (2007) 22 p.  Zbl1176.68099
  16. P. Bouyer, T. Brihaye, M. Jurdziński, R. Lazić and M. Rutkowski, Average-price and reachability-price games on hybrid automata with strong resets. In FORMATS'08: Formal Modelling and Analysis of Timed Systems. Lect. Notes Comput. Sci.5215 (2008).  Zbl1171.68523
  17. T. Brihaye, A note on the undecidability of the reachability problem for o-minimal dynamical systems. Mathematical Logic Quarterly52 (2006) 165–170.  Zbl1089.03035
  18. T. Brihaye, Verification and Control of O-Minimal Hybrid Systems and Weighted Timed Automata, thèse de doctorat. Université Mons-Hainaut, Belgium (2006).  
  19. T. Brihaye and C. Michaux, On the expressiveness and decidability of o-minimal hybrid systems. J. Complexity21 (2005) 447–478.  Zbl1101.68059
  20. T. Brihaye, C. Michaux, C. Rivière and C. Troestler, On o-minimal hybrid systems. In HSCC'04: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.2993 (2004) 219–233.  Zbl1135.93353
  21. V. Bruyère, G. Hansel, C. Michaux and R. Villemaire. Logic and p-recognizable sets of integers. Journées Montoises, Mons (1992). Bull. Belg. Math. Soc. Simon Stevin1 (1994) 191–238.  Zbl0804.11024
  22. A. Casagrande, P. Corvaja, C. Piazza and B. Mishra, Composing semi-algebraic o-minimal automata. In HSCC'07: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.4416 (2007) 668–671.  Zbl1207.93064
  23. C.-C. Chang and H.J. Keisler, Model theory. Studies in Logic and the Foundations of Mathematics, Vol. 73. North-Holland Publishing Co., Amsterdam (1973).  Zbl0276.02032
  24. E.M. Clarke and E.A. Emerson, Design and synthesis of synchronous skeletons using branching-time temporal logic. In Proc. 3rd Workshop Logics of Programs (LOP'81). Lect. Notes Comput. Sci.131 (1981) 52–71.  
  25. C. Dima, Kleene theorems for event-clock automata. In FCT'99: Fundamentals of Computation Theory. Lect. Notes Comput. Sci.1684 (1999) 215–225.  
  26. C. Dima, Real-time automata. J. Autom. Lang. Comb.6 (2001) 3–24.  Zbl0970.68088
  27. L.V. den Dries, Tame Topology and O-Minimal Structures, London Mathematical Society Lecture Note Series 248. Cambridge University Press (1998).  
  28. O. Finkel, Undecidable problems about timed automata. In FORMATS'06: Formal Modeling and Analysis of Timed Systems. Lect. Notes Comput. Sci.4202 (2006) 187–199.  
  29. T.A. Henzinger, The theory of hybrid automata. In LICS'96: Logic in Computer Science. IEEE Computer Society Press (1996) 278–292.  Zbl0959.68073
  30. T.A. Henzinger, P.-H. Ho and H.W.-Toi, A user guide to HyTech. In TACAS'95: Tools and Algorithms for the Construction and Analysis of Systems. Lect. Notes Comput. Sci.1019 (1995) 41–71.  
  31. T.A. Henzinger, P.W. Kopke, A. Puri and P. Varaiya, What's decidable about hybrid automata. J. Comput. System Sci.57 (1998) 94–124.  Zbl0920.68091
  32. P. Herrmann, Timed automata and recognizability. Inform. Process. Lett.65 (1998) 313–318.  Zbl0925.68275
  33. W. Hodges, Model theory, Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press (1993).  
  34. W. Hodges, A shorter model theory. Cambridge University Press (1997).  Zbl0873.03036
  35. J.F. Knight, A. Pillay and C. Steinhorn, Definable sets in ordered structures. II. Trans. Amer. Math. Soc.295 (1986) 593–605.  Zbl0662.03024
  36. G. Lafferriere, G.J. Pappas and S. Yovine, A new class of decidable hybrid systems. In HSCC'99: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.1569 (1999) 137–151.  Zbl0926.93036
  37. G. Lafferriere, G.J. Pappas and S. Sastry, O-minimal hybrid systems. Math. Control Signals Syst.13 (2000) 1–21.  Zbl1059.68073
  38. K.G. Larsen, P. Pettersson and W. Yi, Uppaal: Status & developments. In CAV'97: Computer Aided Verification. Lect. Notes Comput. Sci.1254 (1997) 456–459.  
  39. X.D. Li, T. Zheng, J.M. Hou, J.H. Zhao and G.L. Zheng, Hybrid regular expressions. In Proceedings of the First International Workshop on Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.1386 (1998) 384–399.  
  40. D. Marker, Model theory, Graduate Texts in Mathematics 217. Springer-Verlag, New York (2002).  Zbl1003.03034
  41. J.S. Miller, Decidability and complexity results for timed automata and semi-linear hybrid automata. In HSCC'00: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci.1790 (2000) 296–309.  Zbl0992.93050
  42. A. Pillay and C. Steinhorn, Definable sets in ordered structures. I. Trans. Amer. Math. Soc.295 (1986) 565–592.  Zbl0662.03023
  43. A. Pnueli, The temporal logic of programs. In Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS'77), IEEECSP (1977) 46–57.  
  44. J.-P. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR. In Proc. 5th Intl Symp. on Programming (SOP'82). Lect. Notes Comput. Sci.137 (1982) 337–351.  Zbl0482.68028
  45. G.E. Sacks, Saturated model theory. W.A. Benjamin, Inc., Reading, Mass. Mathematics Lecture Notes Series (1972).  Zbl0242.02054
  46. S. Tripakis, Folk theorems on the determinization and minimization of timed automata. Inform. Process. Lett.99 (2006) 222–226.  Zbl1185.68401
  47. V. Weispfenning, Mixed real-integer linear quantifier elimination. In Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (Vancouver, BC) (electronic). ACM, New York (1999) 129–136.  
  48. A.J. Wilkie, Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. J. Amer. Math. Soc.9 (1996) 1051–1094.  Zbl0892.03013

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.