# 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

## Access Full Article

top## Abstract

top## How to cite

topBrihaye, 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- 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
- R. Alur and D. Dill, A theory of timed automata. Theoret. Comput. Sci.126 (1994) 183–235. Zbl0803.68071
- 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
- R. Alur, C. Courcoubetis and D.L. Dill, Model-checking in dense real-time. Inform. Comput.104 (1993) 2–34. Zbl0783.68076
- 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
- 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
- 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
- E. Asarin, P. Caspi and O. Maler, A kleene theorem for timed automata. In LICS (1997) 160–171.
- 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
- 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
- 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
- P. Bouyer and A. Petit, A Kleene/büchi-like theorem for clock languages. J. Autom. Lang. Comb.7 (2002) 167–186. Zbl1031.68121
- 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).
- 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
- 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
- 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
- T. Brihaye, A note on the undecidability of the reachability problem for o-minimal dynamical systems. Mathematical Logic Quarterly52 (2006) 165–170. Zbl1089.03035
- T. Brihaye, Verification and Control of O-Minimal Hybrid Systems and Weighted Timed Automata, thèse de doctorat. Université Mons-Hainaut, Belgium (2006).
- T. Brihaye and C. Michaux, On the expressiveness and decidability of o-minimal hybrid systems. J. Complexity21 (2005) 447–478. Zbl1101.68059
- 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
- 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
- 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
- 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
- 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.
- C. Dima, Kleene theorems for event-clock automata. In FCT'99: Fundamentals of Computation Theory. Lect. Notes Comput. Sci.1684 (1999) 215–225.
- C. Dima, Real-time automata. J. Autom. Lang. Comb.6 (2001) 3–24. Zbl0970.68088
- L.V. den Dries, Tame Topology and O-Minimal Structures, London Mathematical Society Lecture Note Series 248. Cambridge University Press (1998).
- 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.
- T.A. Henzinger, The theory of hybrid automata. In LICS'96: Logic in Computer Science. IEEE Computer Society Press (1996) 278–292. Zbl0959.68073
- 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.
- 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
- P. Herrmann, Timed automata and recognizability. Inform. Process. Lett.65 (1998) 313–318. Zbl0925.68275
- W. Hodges, Model theory, Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press (1993).
- W. Hodges, A shorter model theory. Cambridge University Press (1997). Zbl0873.03036
- J.F. Knight, A. Pillay and C. Steinhorn, Definable sets in ordered structures. II. Trans. Amer. Math. Soc.295 (1986) 593–605. Zbl0662.03024
- 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
- G. Lafferriere, G.J. Pappas and S. Sastry, O-minimal hybrid systems. Math. Control Signals Syst.13 (2000) 1–21. Zbl1059.68073
- 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.
- 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.
- D. Marker, Model theory, Graduate Texts in Mathematics 217. Springer-Verlag, New York (2002). Zbl1003.03034
- 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
- A. Pillay and C. Steinhorn, Definable sets in ordered structures. I. Trans. Amer. Math. Soc.295 (1986) 565–592. Zbl0662.03023
- A. Pnueli, The temporal logic of programs. In Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS'77), IEEECSP (1977) 46–57.
- 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
- G.E. Sacks, Saturated model theory. W.A. Benjamin, Inc., Reading, Mass. Mathematics Lecture Notes Series (1972). Zbl0242.02054
- S. Tripakis, Folk theorems on the determinization and minimization of timed automata. Inform. Process. Lett.99 (2006) 222–226. Zbl1185.68401
- 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.
- 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 ?

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