Skip to main content
SpringerLink
Log in

Polynomial Interrupt Timed Automata

  • Conference paper
  • First Online:
Book cover Reachability Problems (RP 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9328))

Included in the following conference series:

Abstract

Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (polITA). We prove that reachability is decidable in 2EXPTIME on polITA, using an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of polITA.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 104, 2–34 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS 138, 3–34 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88(7), 971–984 (2000)

    Article  Google Scholar 

  5. Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. TCS 138(1), 35–65 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  6. Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer (2006)

    Google Scholar 

  7. Ben-Or, M., Kozen, D., Reif, J.: The complexity of elementary algebra and geometry. In: Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, STOC 1984, pp. 457–464. ACM (1984)

    Google Scholar 

  8. Bérard, B., Haddad, S.: Interrupt timed automata. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 197–211. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Bérard, B., Haddad, S., Jovanović, A., Lime, D.: Parametric interrupt timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 59–69. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Bérard, B., Haddad, S., Sassolas, M.: Interrupt timed automata: Verification and expressiveness. Formal Methods in System Design 40(1), 41–87 (2012)

    Article  MATH  Google Scholar 

  11. Bérard, B., Haddad, S., Picaronny, C., Safey El Din, M., Sassolas, M.: Polynomial interrupt timed automata. CoRR abs/1504.04541, April 2015

    Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages 2nd GI Conference, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  14. Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.): HS 1991 and HS 1992. LNCS, vol. 736. Springer, Heidelberg (1993)

    Google Scholar 

  15. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hong, H., Din, M.S.E.: Variant quantifier elimination. Journal of Symbolic Computation 47(7), 883–901 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  17. Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. MCSS 13(1), 1–21 (2000)

    MathSciNet  MATH  Google Scholar 

  18. Miller, D.J.: Constructing o-minimal structures with decidable theories using generic families of functions from quasianalytic classes. ArXiv e-prints 1008.2575, August 2010

    Google Scholar 

  19. Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296–309. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  20. Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233–244 (2004)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Sorbonne Université, Université P. & M. Curie, LIP6, ParaSol Project, UMR 7606, Paris, France

    Béatrice Bérard & Mohab Safey El Din

  2. École Normale Supérieure de Cachan, LSV, UMR 8643, INRIA, Cachan, France

    Serge Haddad & Claudine Picaronny

  3. Université Paris-Est, LACL, Créteil, France

    Mathieu Sassolas

  4. CNRS, Cachan, France

    Béatrice Bérard, Serge Haddad, Claudine Picaronny & Mohab Safey El Din

  5. INRIA, Paris-Rocquencourt Center, PolSys Project, Paris, France

    Serge Haddad, Claudine Picaronny & Mohab Safey El Din

Authors
  1. Béatrice Bérard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Serge Haddad
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Claudine Picaronny
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mohab Safey El Din
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mathieu Sassolas
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Serge Haddad .

Editor information

Editors and Affiliations

  1. The Institute of Informatics, University of Warsaw, Warsaw, Poland

    Mikolai Bojanczyk

  2. The Institute of Informatics, University of Warsaw, Warsaw, Poland

    Slawomir Lasota

  3. University of Liverpool, Liverpool, United Kingdom

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Bérard, B., Haddad, S., Picaronny, C., El Din, M.S., Sassolas, M. (2015). Polynomial Interrupt Timed Automata. In: Bojanczyk, M., Lasota, S., Potapov, I. (eds) Reachability Problems. RP 2015. Lecture Notes in Computer Science(), vol 9328. Springer, Cham. https://doi.org/10.1007/978-3-319-24537-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24537-9_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24536-2

  • Online ISBN: 978-3-319-24537-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation