Reachability Problems on Extended O-Minimal Hybrid Automata

  • Raffaella Gentilini
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


Within hybrid systems theory, o-minimal automata are often considered on the border between decidability and undecidability. In such classes of hybrid automata, the constraint of having only constant reset upon discrete jumps is a strong limitation for their applicability: hence, an important issue for both theoreticians and practitioners, is that of relaxing the above constraint, while not fall into undecidability.

In this paper we start considering the problem of timed-bounded reachability on o-minimal automata. This can be seen either as a reachability problem paired with time-constraints or as a classical reachability problem for a class of hybrid automata which properly extends the o-minimal one, with an extra variable representing time. Then, we directly face the problem of extending o-minimal automata by allowing some variables to retain their values upon a discrete jump, without crossing the undecidability border.


Hybrid System Label Transition System Discrete Transition Hybrid Automaton Reachability Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88, 971–984 (2000)CrossRefGoogle Scholar
  3. 3.
    Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Proceedings of the 4th International Workshop on Hybrid Systems, pp. 49–62. Springer, Heidelberg (2001)Google Scholar
  4. 4.
    Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition i: the basic algorithm. SIAM J. Comput. 13(4), 865–877 (1984)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Proceedings of the 4th International Workshop on Hybrid Systems, pp. 147–161. Springer, Heidelberg (2001)Google Scholar
  6. 6.
    Brihaye, T., Michaux, C., Rivire, C., Troestler, C.: On o-minimal hybrid systems. In: Proceedings of the 7-th International Workshop on Hybrid Systems, pp. 219–233 (2004)Google Scholar
  7. 7.
    Davoren, J.M.: Topologies, continuity and bisimulations. Theoretical Informatics and Applications 33(4/5), 357–381 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Gentilini, R.: Reachability problems on extended o-minimal hybrid automata. RR 07-05, Dep. of Computer Science, University of Udine, Italy (2005)Google Scholar
  9. 9.
    Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proceedings of the 36th Annual Symposium on Foundations of Computer Science, p. 453. IEEE, Los Alamitos (1995)Google Scholar
  10. 10.
    Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences 170, pp. 265–292. Springer, Heidelberg (2000)Google Scholar
  11. 11.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proceedings of the 27th Annual Symposium on Theory of Computing, pp. 373–382. ACM Press, New York (1995)Google Scholar
  12. 12.
    Kopke, P.W.: The Theory of Rectangular Hybrid Automata. PhD thesis, Cornell University (1996)Google Scholar
  13. 13.
    Lafferriere, G., Pappas, G., Sastry, S.: O-minimal hybrid systems. Mathematics of Control, Signals, and Systems 13, 1–21 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Lafferriere, G., Pappas, J.G., Yovine, S.: A new class of decidable hybrid systems. In: Proceedings of the Second International Workshop on Hybrid Systems, pp. 137–151. Springer, Heidelberg (1999)Google Scholar
  15. 15.
    Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Proceedings of the Third International Workshop on Hybrid Systems, pp. 296–309 (2000)Google Scholar
  16. 16.
    Courcoubetis, C., Alur, R., Henzinger, T.A.: Computing accumulated delays in real-time systems. Formal Methods in System Design 11, 137–156 (1997)CrossRefGoogle Scholar
  17. 17.
    Tarski, A.: A decision method for elementary algebra and geometry (1951)Google Scholar
  18. 18.
    van den Dries, L.: O-minimal structures. In: Hodges, W. (ed.) Logic: From Foundations to Applications, pp. 99–108. Clarendon Press (1996)Google Scholar
  19. 19.
    van den Dries, L.: Tame topology and o-minimal structures. London Math. Soc. Lecture Note Ser., vol. 248. Cambridge University Press, Cambridge (1998)zbMATHCrossRefGoogle Scholar
  20. 20.
    Wilkie, A.J.: Schanuel conjecture and the decidability of the real exponential field. In: Algebraic Model Theory, pp. 223–230 (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Raffaella Gentilini
    • 1
  1. 1.Università di Udine (DIMI)UdineItaly

Personalised recommendations