Formal language properties of hybrid systems with strong resets
Brihaye, Thomas ; Bruyère, Véronique ; Render, Elaine
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 44 (2010), p. 79-111 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)

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.

Publié le : 2010-01-01
DOI : https://doi.org/10.1051/ita/2010006
Classification:  68Q68,  68Q45 
@article{ITA_2010__44_1_79_0,
     author = {Brihaye, Thomas and Bruy\`ere, V\'eronique and Render, Elaine},
     title = {Formal language properties of hybrid systems with strong resets},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {44},
     year = {2010},
     pages = {79-111},
     doi = {10.1051/ita/2010006},
     mrnumber = {2604936},
     zbl = {1184.68309},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_2010__44_1_79_0}
}

Brihaye, Thomas; Bruyère, Véronique; Render, Elaine. Formal language properties of hybrid systems with strong resets. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 44 (2010) pp. 79-111. doi : 10.1051/ita/2010006. http://gdmltest.u-ga.fr/item/ITA_2010__44_1_79_0/

[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. | Zbl 0765.68150

[2] R. Alur and D. Dill, A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. | Zbl 0803.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. | Zbl 1105.68057

[4] R. Alur, C. Courcoubetis and D.L. Dill, Model-checking in dense real-time. Inform. Comput. 104 (1993) 2-34. | Zbl 0783.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. | Zbl 0874.68206

[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. | Zbl 0912.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. | Zbl 0991.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. | Zbl 0902.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. | Zbl 0991.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. | Zbl 0930.68077

[12] P. Bouyer and A. Petit, A Kleene/büchi-like theorem for clock languages. J. Autom. Lang. Comb. 7 (2002) 167-186. | Zbl 1031.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. | Zbl 1132.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. | Zbl 1176.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). | Zbl 1171.68523

[17] T. Brihaye, A note on the undecidability of the reachability problem for o-minimal dynamical systems. Mathematical Logic Quarterly 52 (2006) 165-170. | Zbl 1089.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. Complexity 21 (2005) 447-478. | Zbl 1101.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. | Zbl 1135.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 Stevin 1 (1994) 191-238. | Zbl 0804.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. | Zbl 1207.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). | Zbl 0276.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. | Zbl 0546.68014

[25] C. Dima, Kleene theorems for event-clock automata. In FCT'99: Fundamentals of Computation Theory. Lect. Notes Comput. Sci. 1684 (1999) 215-225. | Zbl 0948.68106

[26] C. Dima, Real-time automata. J. Autom. Lang. Comb. 6 (2001) 3-24. | Zbl 0970.68088

[27] L.V. Den Dries, Tame Topology and O-Minimal Structures, London Mathematical Society Lecture Note Series 248. Cambridge University Press (1998). | Zbl 0953.03045

[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. | Zbl 1141.68433

[29] T.A. Henzinger, The theory of hybrid automata. In LICS'96: Logic in Computer Science. IEEE Computer Society Press (1996) 278-292. | Zbl 0959.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. | Zbl 0920.68091

[32] P. Herrmann, Timed automata and recognizability. Inform. Process. Lett. 65 (1998) 313-318. | Zbl 0925.68275

[33] W. Hodges, Model theory, Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press (1993). | Zbl 0789.03031

[34] W. Hodges, A shorter model theory. Cambridge University Press (1997). | Zbl 0873.03036

[35] J.F. Knight, A. Pillay and C. Steinhorn, Definable sets in ordered structures. II. Trans. Amer. Math. Soc. 295 (1986) 593-605. | Zbl 0662.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. | Zbl 0926.93036

[37] G. Lafferriere, G.J. Pappas and S. Sastry, O-minimal hybrid systems. Math. Control Signals Syst. 13 (2000) 1-21. | Zbl 1059.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). | Zbl 1003.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. | Zbl 0992.93050

[42] A. Pillay and C. Steinhorn, Definable sets in ordered structures. I. Trans. Amer. Math. Soc. 295 (1986) 565-592. | Zbl 0662.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. | Zbl 0482.68028

[45] G.E. Sacks, Saturated model theory. W.A. Benjamin, Inc., Reading, Mass. Mathematics Lecture Notes Series (1972). | Zbl 0242.02054

[46] S. Tripakis, Folk theorems on the determinization and minimization of timed automata. Inform. Process. Lett. 99 (2006) 222-226. | Zbl 1185.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. | Zbl 0892.03013