Skip to main content
SpringerLink
Log in

LTL Parameter Synthesis of Parametric Timed Automata

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2016)

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

Included in the following conference series:

Abstract

The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL model checking of timed automata. To justify the usefulness of our approach, we provide experimental evaluation and compare our method with explicit enumeration technique.

N. Beneš—The author has been supported by the Czech Science Foundation grant no. GA15-11089S.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST, pp. 125–126. IEEE (2006)

    Google Scholar 

  5. Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, pp. 592–601. ACM (1993)

    Google Scholar 

  6. 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, p. 296. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Beneš, N., Bezděk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 69–81. Springer, Heidelberg (2015)

    Google Scholar 

  8. Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Logic Algebraic Programm. 52, 183–220 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Methods Syst. Des. 35(2), 121–151 (2009)

    Article  MATH  Google Scholar 

  10. Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)

    Article  Google Scholar 

  11. Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed büchi automata emptiness efficiently. Formal Methods Syst. Des. 26(3), 267–292 (2005)

    Article  MATH  Google Scholar 

  12. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  13. Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods Syst. Des. 24(3), 281–320 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  14. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3), 204–215 (2006)

    Article  MATH  Google Scholar 

  15. Li, G.: Checking timed Büchi automata emptiness using LU-abstractions. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 228–242. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Bezděk, P., Beneš, N., Barnat, J., Černá, I.: LTL parameter synthesis of parametric timed automata. CoRR abs/1409.3696 (2016)

    Google Scholar 

  17. Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV. LNCS, vol. 531, pp. 233–242. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  18. Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Programm. 72(1–2), 3–21 (2008)

    Article  MathSciNet  Google Scholar 

  19. Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 53. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  20. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Bezděk, P., Beneš, N., Havel, V., Barnat, J., Černá, I.: On clock-aware LTL properties of timed automata. In: Ciobanu, G., Méry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 43–60. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Informatics, Masaryk University, Brno, Czech Republic

    Peter Bezděk, Nikola Beneš, Jiří Barnat & Ivana Černá

Authors
  1. Peter Bezděk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nikola Beneš
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jiří Barnat
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ivana Černá
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Bezděk .

Editor information

Editors and Affiliations

  1. IMT - School for Advanced Studies, Lucca, Italy

    Rocco De Nicola

  2. Institute of Computer Languages, TU Wien, Wien, Austria

    Eva Kühn

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Bezděk, P., Beneš, N., Barnat, J., Černá, I. (2016). LTL Parameter Synthesis of Parametric Timed Automata. In: De Nicola, R., Kühn, E. (eds) Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science(), vol 9763. Springer, Cham. https://doi.org/10.1007/978-3-319-41591-8_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41591-8_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41590-1

  • Online ISBN: 978-3-319-41591-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation