Formal language properties of hybrid systems with strong resets
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 44 (2010) no. 1, pp. 79-111.

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.

DOI : 10.1051/ita/2010006
Classification : 68Q68, 68Q45
Mots-clés : hybrid systems with strong resets, formal language theory 
@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},
     pages = {79--111},
     publisher = {EDP-Sciences},
     volume = {44},
     number = {1},
     year = {2010},
     doi = {10.1051/ita/2010006},
     mrnumber = {2604936},
     zbl = {1184.68309},
     language = {en},
     url = {http://archive.numdam.org/articles/10.1051/ita/2010006/}
}
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 - Informatique Théorique et Applications
PY  - 2010
SP  - 79
EP  - 111
VL  - 44
IS  - 1
PB  - EDP-Sciences
UR  - http://archive.numdam.org/articles/10.1051/ita/2010006/
DO  - 10.1051/ita/2010006
LA  - en
ID  - ITA_2010__44_1_79_0
ER  - 
%0 Journal Article
%A Brihaye, Thomas
%A Bruyère, Véronique
%A Render, Elaine
%T Formal language properties of hybrid systems with strong resets
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2010
%P 79-111
%V 44
%N 1
%I EDP-Sciences
%U http://archive.numdam.org/articles/10.1051/ita/2010006/
%R 10.1051/ita/2010006
%G en
%F 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) no. 1, pp. 79-111. doi : 10.1051/ita/2010006. http://archive.numdam.org/articles/10.1051/ita/2010006/

[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

[2] R. Alur and D. Dill, A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. | Zbl

[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

[4] R. Alur, C. Courcoubetis and D.L. Dill, Model-checking in dense real-time. Inform. Comput. 104 (1993) 2-34. | Zbl

[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

[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

[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

[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

[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

[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

[12] P. Bouyer and A. Petit, A Kleene/büchi-like theorem for clock languages. J. Autom. Lang. Comb. 7 (2002) 167-186. | Zbl

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

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

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

[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

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

[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

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

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

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

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

[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

[37] G. Lafferriere, G.J. Pappas and S. Sastry, O-minimal hybrid systems. Math. Control Signals Syst. 13 (2000) 1-21. | Zbl

[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

[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

[42] A. Pillay and C. Steinhorn, Definable sets in ordered structures. I. Trans. Amer. Math. Soc. 295 (1986) 565-592. | Zbl

[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

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

[46] S. Tripakis, Folk theorems on the determinization and minimization of timed automata. Inform. Process. Lett. 99 (2006) 222-226. | Zbl

[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

Cité par Sources :