SMT-Based Parameter Synthesis for Parametric Timed Automata

  • Michał Knapik
  • Wojciech Penczek
Part of the Studies in Computational Intelligence book series (SCI, volume 634)


We present a simple method for representing finite executions of Parametric Timed Automata using Satisfiability Modulo Theories (SMT). The transition relation of an automaton is translated to a formula of SMT, which is used to represent all the prefixes of a given length of all the executions. This enables to underapproximate the set of parameter valuations for the undecidable problem of parametric reachability. We introduce a freely available, open-source tool PTA2SMT and show its application to the synthesis of parameter valuations under which a timed mutual exclusion protocol fails.


Model Check Mutual Exclusion Propositional Variable Label Transition System Parameter Synthesis 
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.



Michał Knapik is supported by the Foundation for Polish Science under Int. Ph.D. Projects in Intelligent Computing. Project financed from the EU within the Innovative Economy OP 2007–2013 and ERDF.


  1. 1.
    Alur, R., Henzinger, T., Vardi, M.: Parametric real-time reasoning. In: Proceedings of the 25th Annual Symposium on Theory of Computing, pp. 592–601. ACM (1993)Google Scholar
  2. 2.
    André, É., Chatain, T., Fribourg, L., Encrenaz, E.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819–836 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report. Department of Computer Science, The University of Iowa, available at (2010)
  4. 4.
    Barrett, C., Tinelli, C.: CVC3. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4590, pp. 298–302. Springer, Berlin (2007)Google Scholar
  5. 5.
    Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Form. Methods Syst. Des. 35(2), 121–151 (2009).
  6. 6.
    de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: an appetizer. Formal Methods: Foundations and Applications. In: 12th Brazilian Symposium on Formal Methods, (SBMF), Revised Selected Papers. Lecture Notes in Computer Science, vol. 5902, pp. 23–36. Springer (2009)Google Scholar
  7. 7.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52–53, 183–220 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 7795, pp. 401–415. Springer (2013)Google Scholar
  9. 9.
  10. 10.
    Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Trans. Petri Nets Models Concurr. 5, 141–159 (2012)CrossRefzbMATHGoogle Scholar
  11. 11.
    Knapik, M., Penczek, W.: SMT-based parameter synthesis for L/U automata. In: Proceedings of the International Workshop on Petri Nets and Software Engineering, vol. 851, pp. 77–92. CEUR, Hamburg, 25–26 June 2012Google Scholar
  12. 12.
    Knapik, M., Penczek, W.: Parameter synthesis for timed Kripke structures. Fundam. Inform. 133(2–3), 211–226 (2014).
  13. 13.
    Knapik, M., Penczek, W., Szreter, M., Pólrola, A.: Bounded parametric verification for distributed time petri nets with discrete-time semantics. Fundam. Inform. 101(1–2), 9–27 (2010)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Knapik, M., Szreter, M., Penczek, W.: Bounded parametric model checking for elementary net systems. Trans. Petri Nets Models Concurr. 4, 42–71 (2010)zbMATHGoogle Scholar
  15. 15.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)CrossRefzbMATHGoogle Scholar
  16. 16.
    Penczek, W., Pólrola, A., Zbrzezny, A.: SAT-based (parametric) reachability for a class of distributed time petri nets. Trans. Petri Nets Models Concurr. 4, 72–97 (2010)zbMATHGoogle Scholar
  17. 17.
    Penczek, W., Szreter, M.: SAT-based unbounded model checking of timed automata. Fundam. Inform. 85(1–4), 425–440 (2008)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Spelberg, R.F.L., Toetenel, W.J.: Splitting trees and partition refinement in real-time model checking. In: 35th Hawaii International Conference on System Sciences (HICSS-35 2002), CD-ROM/Abstracts Proceedings, Big Island, HI, USA. p. 278, IEEE Computer Society, 7–10 January 2002.
  19. 19.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Design 18(1), 25–68 (2001)CrossRefzbMATHGoogle Scholar
  20. 20.
    Wang, F.: Parametric analysis of computer systems. Form. Methods Syst. Design 17(1), 39–60 (2000)CrossRefGoogle Scholar
  21. 21.
    Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundam. Inform. 67(1–3), 303–322 (2005)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Institute of Computer Science, PASWarsawPoland
  2. 2.University of Natural Sciences and Humanities, IISiedlcePoland

Personalised recommendations