Advertisement

Abstract

In this work, we introduce the class of Interrupt Timed Automata (ITA), which are well suited to the description of multi-task systems with interruptions in a single processor environment. This model is a subclass of hybrid automata. While reachability is undecidable for hybrid automata we show that in ITA the reachability problem is in 2-EXPSPACE and in PSPACE when the number of clocks is fixed, with a procedure based on a generalized class graph. Furthermore we consider a subclass ITA which still describes usual interrupt systems and for which the reachability problem is in NEXPTIME and in NP when the number of clocks is fixed (without any class graph). There exist languages accepted by an ITA but neither by timed automata nor by controlled real-time automata (CRTA), another extension of timed automata. However we conjecture that CRTA is not contained in ITA. So, we combine ITA with CRTA in a model which encompasses both classes and show that the reachability problem is still decidable.

Keywords

Hybrid automata timed automata multi-task systems interruptions decidability of reachability 

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Asarin, E., Maler, O., Pnueli, A.: Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives. Theoretical Computer Science 138, 35–66 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Asarin, E., Schneider, G., Yovine, S.: Algorithmic Analysis of Polygonal Hybrid Systems, Part I: Reachability. Theoretical Computer Science 379(1-2), 231–265 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bérard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36, 145–182 (1998)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Brihaye, T., Bruyère, V., Raskin, J.-F.: On Model-Checking Timed Automata with Stopwatch Observers. Information and Computatiion 2004(3), 408–433 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Demichelis, F., Zielonka, W.: Controlled timed automata. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 455–469. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences 57, 94–124 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S.: Decidable Integration Graphs. Information and Computation 150(2), 209–243 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 137–151. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computations for families of linear vector fields. Journal of Symbolic Computation 32(3), 231–253 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Maler, O., Manna, Z., Pnueli, A.: From Timed to Hybrid Systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 447–484. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  15. 15.
    Roos, C., Terlaky, T., Vial, J.-P.: Theory and Algorithms for Linear Optimization. An Interior Point Approach. Wiley-Interscience, John Wiley & Sons Ltd., West Sussex (1997)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Beatrice Bérard
    • 1
  • Serge Haddad
    • 2
  1. 1.Université Pierre & Marie Curie, LIP6/MoVe, CNRS UMRParisFrance
  2. 2.Ecole Normale Supérieure de Cachan, LSV, CNRS UMRCachanFrance

Personalised recommendations