Abstract
Model checking timed systems may be negatively impacted by the presence of Zeno runs as counterexamples. Such runs contain an infinite number of discrete actions occurring in a finite time, which is unrealistic; therefore, these runs must be pruned during model checking. Given a model of a timed system and a property, parametric model checking aims at synthesizing timing valuations such that the model satisfies the property. A popular formalism for parametric timed model checking is parametric timed automata (PTAs), an extension of timed automata with unknown constants. We address the presence of Zeno runs in parametric model checking. We first show that the emptiness of the set of parameter valuations for which at least one counterexample run being non-Zeno is undecidable for PTAs. As a second contribution, we adopt a more pragmatic approach, and propose a procedure based on a transformation of PTAs into Clock Upper Bound PTAs to derive all valuations whenever it terminates, and some of them otherwise. We implemented our algorithm in IMITATOR, and we show that our method can be distributed over a cluster to further speedup the computation.
Similar content being viewed by others
Data availability
The datasets analyzed during the current study are available in the Zenodo repository, at 10.5281/zenodo.7096134.
Notes
Observe that a parametric guard with two upper bounds on \(x\) can be encoded using two consecutive transitions in 0-time.
Our definition is slightly more liberal than the one in [51].
Note that if a clock has more than a single upper bound in a guard, then the minimum can be encoded as a disjunction of constraints, and our results would still apply with non-convex constraints (that can be implemented using a finite list of convex constraints).
This model assumes that, after the change of a signal in the input of a gate, the output changes after a delay which is modeled using a parametric closed interval.
A purely parametric constraint (e. g. \(p_1 > p_2 \wedge p_3 = 3\)) is generally not allowed by the PTA syntax, but can be simulated using appropriate clocks (e. g. \(p_1> x> p_2 \wedge p_3 = x' = 3\)). Such parametric constraints are allowed in the input syntax of IMITATOR.
Following a well-known result for PTAs, all symbolic states belonging to a same cycle in a parametric zone graph necessarily have the same parameter constraint [46].
References
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235. https://doi.org/10.1016/0304-3975(94)90010-8
Alur R, Henzinger TA, Vardi MY (1993) Parametric real-time reasoning. In: Kosaraju SR, Johnson DS, Aggarwal A (eds) STOC. ACM, New York, NY, USA, pp 592–601. https://doi.org/10.1145/167088.167242
André É (2016) Parametric deadlock-freeness checking timed automata. In: Sampaio ACA, Wang F (eds) ICTAC. Lecture Notes in Computer Science, vol. 9965, Springer. pp 469–478. https://doi.org/10.1007/978-3-319-46750-4_27
André É (2019) What’s decidable about parametric timed automata? Int J Softw Tools Technol Transf 21(2):203–219. https://doi.org/10.1007/s10009-017-0467-0
André É, Arcaini P, Gargantini A, Radavelli M (2019) Repairing timed automata clock guards through abstraction and testing. In: Beyer D, Keller C (eds) TAP. Lecture Notes in Computer Science, vol. 11823, Springer. pp 129–146. https://doi.org/10.1007/978-3-030-31157-5_9
André É, Arias J, Petrucci L, van de Pol J (2021) Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In: Groote JF, Larsen KG (eds) TACAS. Lecture Notes in Computer Science, vol. 12651, Springer. pp 311–329. https://doi.org/10.1007/978-3-030-72016-2_17
André É, Chatain Th, De Smet O, Fribourg L, Ruel S (Nov 2009) Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In: Lime D, Roux OH (eds) MSR. Journal Européen des Systèmes Automatisés, vol. 43, Hermès. pp 1049–1064
André É, Chatain Th, Encrenaz E, Fribourg L (2009) An inverse method for parametric timed automata. Int J Found. Comput. Sci. 20(5):819–836. https://doi.org/10.1142/S0129054109006905
André É, Coti C, Evangelista S (2014) Distributed behavioral cartography of timed automata. In: Dongarra J, Ishikawa Y, Atsushi H (eds) EuroMPI/ASIA. ACM, New York. pp 109–114. https://doi.org/10.1145/2642769.2642784
André É, Coti C, Nguyen HG (Nov 2015) Enhanced distributed behavioral cartography of parametric timed automata. In: Butler M, Conchon S, Zaïdi F (eds) ICFEM. Lecture Notes in Computer Science, vol. 9407, Springer. pp 319–335. https://doi.org/10.1007/978-3-319-25423-4_21
André É, Fribourg L, Kühne U, Soulat R (Aug 2012) IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In: Giannakopoulou D, Méry D (eds) FM. Lecture Notes in Computer Science, vol. 7436, Springer. pp 33–36. https://doi.org/10.1007/978-3-642-32759-9_6
André É, Lime D (2017) Liveness in L/U-parametric timed automata. In: Legay A, Schneider K (eds) ACSD. IEEE. pp 9–18. https://doi.org/10.1109/ACSD.2017.19
André É, Lime D, Markey N (Jan 2020) Language preservation problems in parametric timed automata. Logical Methods in Comput Sci 16(1): https://doi.org/10.23638/LMCS-16(1:5)2020
André É, Lime D, Roux OH (2016) Decision problems for parametric timed automata. In: Ogata K, Lawford M, Liu S (eds) ICFEM. Lecture Notes in Computer Science, vol. 10009, Springer. pp 400–416. https://doi.org/10.1007/978-3-319-47846-3_25
André É, Lin SW (2017) Learning-based compositional parameter synthesis for event-recording automata. In: Bouajjani A, Alexandra S (eds) FORTE. Lecture Notes in Computer Science, vol. 10321, Springer. pp 17–32. https://doi.org/10.1007/978-3-319-60225-7_2
André É, Liu Y, Sun J, Dong JS (2014) Parameter synthesis for hierarchical concurrent real-time systems. Real-Time Syst 50(5–6):620–679. https://doi.org/10.1007/s11241-014-9208-6
André É, Marinho D, van de Pol J (2021) A benchmarks library for extended timed automata. In: Loulergue F, Wotawa F (eds) TAP. Lecture Notes in Computer Science, vol. 12740, Springer. pp 39–50. https://doi.org/10.1007/978-3-030-79379-1_3
André É, Nguyen HG, Petrucci L, Sun J (2017) Parametric model checking timed automata under non-Zenoness assumption. In: Barrett C, Kahsai T (eds) NFM. Lecture Notes in Computer Science, vol. 10227, Springer. pp 35–51. https://doi.org/10.1007/978-3-319-57288-8_3
Aştefănoaei L, Bensalem S, Bozga M, Cheng C, Ruess H (2016) Compositional parameter synthesis. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM. Lecture Notes in Computer Science, vol. 9995, pp 60–68. https://doi.org/10.1007/978-3-319-48989-6_4
Bagnara R, Hill PM, Zaffanella E (2008) The Parma Polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci Comput Program 72(1–2):3–21. https://doi.org/10.1016/j.scico.2007.08.001
Behrmann G, Bouyer P, Larsen KG, Pelánek R (2006) Lower and upper bounds in zone-based abstractions of timed automata. Int J Softw Tools Technol Transf 8(3):204–215. https://doi.org/10.1007/s10009-005-0190-0
Beneš N, Bezděk P, Larsen KG, Srba J (Jul 2015) Language emptiness of continuous-time parametric timed automata. In: Halldórsson MM, Iwama K, Kobayashi N, Speckmann B (eds) ICALP, Part II. Lecture Notes in Computer Science, vol. 9135, Springer. pp 69–81. https://doi.org/10.1007/978-3-662-47666-6_6
Bengtsson J, Yi W (2003) Timed automata: Semantics, algorithms and tools. In: Desel J, Reisig W, Rozenberg G (eds) Lectures on Concurrency and Petri Nets, Advances in Petri Nets. Lecture Notes in Computer Science, vol. 3098, Springer. pp 87–124. https://doi.org/10.1007/978-3-540-27755-2_3
Beyer D, Lewerentz C, Noack A (2003) Rabbit: A tool for BDD-based verification of real-time systems. In: Jr, WAH, Somenzi F (eds) CAV. Lecture Notes in Computer Science, vol. 2725, Springer. pp 122–125. https://doi.org/10.1007/978-3-540-45069-6_13
Bowman H, Gómez R (2006) How to stop time stop**. Form Asp Comput 18(4):459–493. https://doi.org/10.1007/s00165-006-0010-7
Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: A model-checking tool for real-time systems. In: Hu AJ, Vardi MY (eds) Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998). Lecture Notes in Computer Science, vol. 1427, Springer. pp 546–550. https://doi.org/10.1007/BFb0028779
Bozzelli L, La Torre S (2009) Decision problems for lower/upper bound parametric timed automata. Form Methods Syst Des 35(2):121–151. https://doi.org/10.1007/s10703-009-0074-0
Clarisó R, Cortadella J (2005) Verification of concurrent systems with parametric delays using octahedra. In: ACSD. IEEE Computer Society. pp 122–131. https://doi.org/10.1109/ACSD.2005.34
Clarisó R, Cortadella J (2007) The octahedron abstract domain. Sci Comput Program 64(1):115–139. https://doi.org/10.1016/j.scico.2006.03.009
Collomb-Annichini A, Sighireanu M (2001) Parameterized reachability analysis of the IEEE 1394 root contention protocol using TReX. In: RT-TOOLS
Dong JS, Hao P, Qin S, Sun J, Yi W (2008) Timed automata patterns. IEEE Trans Softw Eng 34(6):844–859. https://doi.org/10.1109/TSE.2008.52
Evangelista S, Laarman A, Petrucci L, van de Pol J (2012) Improved multi-core nested depth-first search. In: Chakraborty S, Mukund M (eds) ATVA. Lecture Notes in Computer Science, vol. 7561. Springer. pp 269–283. https://doi.org/10.1007/978-3-642-33386-6_22
Gómez R, Bowman H (2007) Efficient detection of Zeno runs in timed automata. In: Raskin JF, Thiagarajan PS (eds) FORMATS. Lecture Notes in Computer Science, vol. 4763, Springer. pp 195–210. https://doi.org/10.1007/978-3-540-75454-1_15
Herbreteau F, Srivathsan B, Walukiewicz I (2012) Efficient emptiness check for timed Büchi automata. Form Methods Syst Des 40(2):122–146. https://doi.org/10.1007/s10703-011-0133-1
Hune T, Romijn J, Stoelinga M, Vaandrager FW (2002) Linear parametric model checking of timed automata. J Logic Algebraic Program 52–53:183–220. https://doi.org/10.1016/S1567-8326(02)00037-1
Jovanović A, Lime D, Roux OH (2015) Integer parameter synthesis for real-time systems. IEEE Trans Softw Eng 41(5):445–461. https://doi.org/10.1109/TSE.2014.2357445
Knapik M, Penczek W (2012) Bounded model checking for parametric timed automata. Trans Petri Nets Other Models Concurr 5:141–159. https://doi.org/10.1007/978-3-642-29072-5_6
Kwiatkowska MZ, Norman G, Sproston J, Wang F (2007) Symbolic model checking for probabilistic timed automata. Inf Comput 205(7):1027–1077. https://doi.org/10.1016/j.ic.2007.01.004
Laarman A, Olesen MC, Dalsgaard AE, Larsen KG, van De Pol J (Jul 2013) Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In: Sharygina N, Veith H (eds) CAV. Lecture Notes in Computer Science, vol. 8044. Springer. pp 968–983. Heidelberg, Germany. https://doi.org/10.1007/978-3-642-39799-8_69
Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1–2):134–152. https://doi.org/10.1007/s100090050010
Lipari G, Sun Y, André É, Fribourg L (Apr 2014) Toward parametric timed interfaces for real-time components. In: André E, Frehse G (eds) SynCoP. Electronic Proceedings in Theoretical Computer Science, vol. 145, pp 49–64. https://doi.org/10.4204/EPTCS.145.6, http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?145.6.pdf
Luthmann L, Gerecht T, Stephan A, Bürdek J, Lochau M (2019) Minimum/maximum delay testing of product lines with unbounded parametric real-time constraints. J Syst Softw 149:535–553. https://doi.org/10.1016/j.jss.2018.12.028
Luthmann L, Stephan A, Bürdek J, Lochau M (2017) Modeling and testing product lines with unbounded parametric real-time constraints. In: Cohen MB, Acher M, Fuentes L, Schall D, Bosch J, Capilla R, Bagheri E, **ong Y, Troya J, Cortés AR, Benavides D (eds) SPLC, Volume A, ACM. pp 104–113. https://doi.org/10.1145/3106195.3106204
Miller JS (2000) Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch NA, Krogh BH (eds) HSCC. Lecture Notes in Computer Science, vol. 1790, Springer. pp 296–309. https://doi.org/10.1007/3-540-46430-1_26
Minsky ML (1967) Computation: finite and infinite machines. Prentice-Hall Inc, Upper Saddle River, NJ, USA
Nguyen HG, Petrucci L, van de Pol J (Dec 2018) Layered and collecting NDFS with subsumption for parametric timed automata. In: Lin AW, Sun J (eds) ICECCS. pp 1–9. IEEE Computer Society. https://doi.org/10.1109/ICECCS2018.2018.00009
Sun J, Liu Y, Dong JS, Pang J (2009) PAT: Towards flexible verification under fairness. In: Bouajjani A, Maler O (eds) CAV. Lecture Notes in Computer Science, vol. 5643, Springer. pp 709–714. https://doi.org/10.1007/978-3-642-02658-4_59
Tripakis S (1999) Verifying progress in timed systems. In: Katoen JP (ed) ARTS. Lecture Notes in Computer Science, vol. 1601. Springer, New York. pp 299–314
Tripakis S, Yovine S, Bouajjani A (2005) Checking timed Büchi automata emptiness efficiently. Form Methods Syst Des 26(3):267–292. https://doi.org/10.1007/s10703-005-1632-8
Wang F (2001) Symbolic verification of complex real-time systems with clock-restriction diagram. In: Kim M, Chin B, Kang S, Lee D (eds) FORTE. IFIP Conference Proceedings, vol. 197, Kluwer. pp 235–250
Wang T, Sun J, Wang X, Liu Y, Si Y, Dong JS, Yang X, Li X (2015) A systematic study on explicit-state non-Zenoness checking for timed automata. IEEE Trans Softw Eng 41(1):3–18. https://doi.org/10.1109/TSE.2014.2359893
Acknowledgements
We would like to thank the anonymous reviewers for useful comments.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015) and by the ANR national research program BisoUS.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
André, É., Nguyen, H.G., Petrucci, L. et al. Distributed parametric model checking timed automata under non-Zenoness assumption. Form Methods Syst Des 59, 253–290 (2021). https://doi.org/10.1007/s10703-022-00400-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-022-00400-z