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.  
  2. R. Alur and D. Dill, A theory of timed automata. Theoret. Comput. Sci.126 (1994) 183–235.  
  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.  
  4. R. Alur, C. Courcoubetis and D.L. Dill, Model-checking in dense real-time. Inform. Comput.104 (1993) 2–34.  
  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.  
  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.  
  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.  
  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.  
  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.  
  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.  
  12. P. Bouyer and A. Petit, A Kleene/büchi-like theorem for clock languages. J. Autom. Lang. Comb.7 (2002) 167–186.  
  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.  
  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.  
  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).  
  17. T. Brihaye, A note on the undecidability of the reachability problem for o-minimal dynamical systems. Mathematical Logic Quarterly52 (2006) 165–170.  
  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.  
  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.  
  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.  
  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.  
  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).  
  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.  
  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.  
  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.  
  32. P. Herrmann, Timed automata and recognizability. Inform. Process. Lett.65 (1998) 313–318.  
  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).  
  35. J.F. Knight, A. Pillay and C. Steinhorn, Definable sets in ordered structures. II. Trans. Amer. Math. Soc.295 (1986) 593–605.  
  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.  
  37. G. Lafferriere, G.J. Pappas and S. Sastry, O-minimal hybrid systems. Math. Control Signals Syst.13 (2000) 1–21.  
  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).  
  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.  
  42. A. Pillay and C. Steinhorn, Definable sets in ordered structures. I. Trans. Amer. Math. Soc.295 (1986) 565–592.  
  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.  
  45. G.E. Sacks, Saturated model theory. W.A. Benjamin, Inc., Reading, Mass. Mathematics Lecture Notes Series (1972).  
  46. S. Tripakis, Folk theorems on the determinization and minimization of timed automata. Inform. Process. Lett.99 (2006) 222–226.  
  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.  

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.