Hostname: page-component-586b7cd67f-r5fsc Total loading time: 0 Render date: 2024-11-24T19:36:54.260Z Has data issue: false hasContentIssue false
  • English
  • Français

Formal language properties of hybrid systems with strong resets

Published online by Cambridge University Press:  11 February 2010

Thomas Brihaye ,
Véronique Bruyère  and
Elaine Render
Thomas Brihaye
Affiliation:
Institute of Mathematics, University of Mons 20, Place du Parc, 7000 Mons, Belgium; [email protected]
Véronique Bruyère
Affiliation:
Institute of Computer Science, University of Mons 20, Place du Parc, 7000 Mons, Belgium; [email protected]
Elaine Render
Affiliation:
School of Mathematics, University of Manchester, Oxford Road, Manchester, U.K.; [email protected]
Get access

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.

Keywords

Hybrid systems with strong resetsformal language theory.
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 44 , Issue 1: Special issue dedicated to the 12th "Journées Montoises d'Informatique Théorique" , January 2010 , pp. 79 - 111
Copyright
© EDP Sciences, 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Alur, R. and Dill, D., Automata for modeling real-time systems. In ICALP'90: Automata, Languages, and Programming. Lect. Notes Comput. Sci. 443 (1990) 322–335. CrossRef
Alur, R. and Dill, D., A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183–235. CrossRef
Alur, R. and Madhusudan, P., Decision problems for timed automata: A survey. In SFM'04: School on Formal Methods. Lect. Notes Computer Sci. 3185 (2004) 1–24. CrossRef
Alur, R., Courcoubetis, C. and Dill, D.L., Model-checking in dense real-time. Inform. Comput. 104 (1993) 2–34. CrossRef
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J. and Yovine, S., The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138 (1995) 3–34. CrossRef
Alur, R., Fix, L. and Henzinger, T.A., Event-clock automata: a determinizable class of timed automata. Theoret. Comput. Sci. 211 (1999) 253–273. CrossRef
Alur, R., La Torre, S. and Pappas, G.J., Optimal paths in weighted timed automata. In HSCC'01: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci. 203 (2001) 449–62.
E. Asarin, P. Caspi and O. Maler, A kleene theorem for timed automata. In LICS (1997) 160–171.
Beauquier, D., Pumping lemmas for timed automata. In Foundations of software science and computation structures (Lisbon, 1998). Lect. Notes Comput. Sci. 1378 (1998) 81–94. CrossRef
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J. and Vaandrager, F., Minimum-cost reachability for priced timed automata. In HSCC'01: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci. 2034 (2001) 147–161. CrossRef
Bérard, B., Petit, A., Diekert, V. and Gastin, P., Characterization of the expressive power of silent transitions in timed automata. Fund. Inform. 36 (1998) 145–182.
Bouyer, P. and Petit, A., Kleene, A/büchi-like theorem for clock languages. J. Autom. Lang. Comb. 7 (2002) 167–186.
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).
Bouyer, P., Brihaye, T. and Chevalier, F., 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. CrossRef
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.
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).
Brihaye, T., A note on the undecidability of the reachability problem for o-minimal dynamical systems. Mathematical Logic Quarterly 52 (2006) 165–170. CrossRef
T. Brihaye, Verification and Control of O-Minimal Hybrid Systems and Weighted Timed Automata, thèse de doctorat. Université Mons-Hainaut, Belgium (2006).
Brihaye, T. and Michaux, C., On the expressiveness and decidability of o-minimal hybrid systems. J. Complexity 21 (2005) 447–478. CrossRef
Brihaye, T., Michaux, C., Rivière, C. and Troestler, C., On o-minimal hybrid systems. In HSCC'04: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci. 2993 (2004) 219–233. CrossRef
Bruyère, V., Hansel, G., Michaux, C. and Villemaire, R.. Logic and p-recognizable sets of integers. Journées Montoises, Mons (1992). Bull. Belg. Math. Soc. Simon Stevin 1 (1994) 191–238.
Casagrande, A., Corvaja, P., Piazza, C. and Mishra, B., Composing semi-algebraic o-minimal automata. In HSCC'07: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci. 4416 (2007) 668–671. CrossRef
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).
Clarke, E.M. and Emerson, E.A., 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.
Dima, C., Kleene theorems for event-clock automata. In FCT'99: Fundamentals of Computation Theory. Lect. Notes Comput. Sci. 1684 (1999) 215–225. CrossRef
Dima, C., Real-time automata. J. Autom. Lang. Comb. 6 (2001) 3–24.
L.V. den Dries, Tame Topology and O-Minimal Structures, London Mathematical Society Lecture Note Series 248. Cambridge University Press (1998).
Finkel, O., Undecidable problems about timed automata. In FORMATS'06: Formal Modeling and Analysis of Timed Systems. Lect. Notes Comput. Sci. 4202 (2006) 187–199. CrossRef
T.A. Henzinger, The theory of hybrid automata. In LICS'96: Logic in Computer Science. IEEE Computer Society Press (1996) 278–292.
Henzinger, T.A., Ho, P.-H. 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. CrossRef
Henzinger, T.A., Kopke, P.W., Puri, A. and Varaiya, P., What's decidable about hybrid automata. J. Comput. System Sci. 57 (1998) 94–124. CrossRef
Herrmann, P., Timed automata and recognizability. Inform. Process. Lett. 65 (1998) 313–318. CrossRef
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).
Knight, J.F., Pillay, A. and Steinhorn, C., Definable sets in ordered structures. II. Trans. Amer. Math. Soc. 295 (1986) 593–605. CrossRef
Lafferriere, G., Pappas, G.J. and Yovine, S., A new class of decidable hybrid systems. In HSCC'99: Hybrid Systems: Computation and Control. Lect. Notes Comput. Sci. 1569 (1999) 137–151. CrossRef
Lafferriere, G., Pappas, G.J. and Sastry, S., O-minimal hybrid systems. Math. Control Signals Syst. 13 (2000) 1–21. CrossRef
Larsen, K.G., Pettersson, P. and Uppaal, W. Yi: Status & developments. In CAV'97: Computer Aided Verification. Lect. Notes Comput. Sci. 1254 (1997) 456–459. CrossRef
Li, X.D., Zheng, T., Hou, J.M., Zhao, J.H. and Zheng, G.L., 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).
Miller, J.S., 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. CrossRef
Pillay, A. and Steinhorn, C., Definable sets in ordered structures. I. Trans. Amer. Math. Soc. 295 (1986) 565–592. CrossRef
A. Pnueli, The temporal logic of programs. In Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS'77), IEEECSP (1977) 46–57.
Queille, J.-P. and Sifakis, J., 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. CrossRef
G.E. Sacks, Saturated model theory. W.A. Benjamin, Inc., Reading, Mass. Mathematics Lecture Notes Series (1972).
Tripakis, S., Folk theorems on the determinization and minimization of timed automata. Inform. Process. Lett. 99 (2006) 222–226. CrossRef
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.
Wilkie, A.J., 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. CrossRef