Reachability Preservation Based Parameter Synthesis for Timed Automata

  • Étienne AndréEmail author
  • Giuseppe Lipari
  • Hoang Gia Nguyen
  • Youcheng Sun
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


The synthesis of timing parameters consists in deriving conditions on the timing constants of a concurrent system such that it meets its specification. Parametric timed automata are a powerful formalism for parameter synthesis, although most problems are undecidable. We first address here the following reachability preservation problem: given a reference parameter valuation and a (bad) control state, do there exist other parameter valuations that reach this control state iff the reference parameter valuation does? We show that this problem is undecidable, and introduce a procedure that outputs a possibly underapproximated answer. We then show that our procedure can efficiently replace the behavioral cartography to partition a bounded parameter subspace into good and bad subparts; furthermore, our procedure can even outperform the classical bad-state driven parameter synthesis semi-algorithm, especially when distributed on a cluster.


Integer Point Parameter Synthesis Symbolic State Time Automaton Constraint Output 
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)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601. ACM (1993)Google Scholar
  3. 3.
    André, É., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819–836 (2009)zbMATHGoogle Scholar
  4. 4.
    André, É., Coti, C., Evangelista, S.: Distributed behavioral cartography of timed automata. In: EuroMPI/ASIA 201414, pp. 109–114. ACM (2014)Google Scholar
  5. 5.
    André, É., Fribourg, L.: Behavioral cartography of timed automata. In: Kučera, A., Potapov, I. (eds.) RP 2010. LNCS, vol. 6227, pp. 76–90. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  6. 6.
    André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  7. 7.
    André, É., Soulat, R.: Synthesis of timing parameters satisfying safety properties. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 31–44. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  8. 8.
    Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design 35(2), 121–151 (2009)CrossRefzbMATHGoogle Scholar
  9. 9.
    Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed state space analysis of real-time preemptive systems. Transactions on Software Engineering 30(2), 97–111 (2004)CrossRefGoogle Scholar
  10. 10.
    Chevallier, R., Encrenaz-Tiphène, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design 34(1), 59–81 (2009)CrossRefzbMATHGoogle Scholar
  11. 11.
    Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165–168. IEEE (2013)Google Scholar
  12. 12.
    Cimatti, A., Palopoli, L., Ramadian, Y.: Symbolic computation of schedulability regions using parametric timed automata. In: RTSS, pp. 80–89. IEEE Computer Society (2008)Google Scholar
  13. 13.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52–53, 183–220 (2002)MathSciNetGoogle Scholar
  14. 14.
    Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Transactions on Software Engineering (2014, to appear)Google Scholar
  15. 15.
    Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multi-core emptiness checking of timed büchi automata using inclusion abstraction. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 968–983. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  16. 16.
    Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Étienne André
    • 1
    Email author
  • Giuseppe Lipari
    • 2
  • Hoang Gia Nguyen
    • 1
  • Youcheng Sun
    • 3
  1. 1.Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030ParisFrance
  2. 2.CRIStAL – UMR 9189Université de Lille, USR 3380 CNRSLilleFrance
  3. 3.Scuola Superiore Sant’AnnaPisaItaly

Personalised recommendations