Abstract
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.
This work is partially supported by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015) and CNRS-INS2I project TrAVAIL.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We used IMITATOR 3.3-beta-2 “Cheese Caramel au beurre salé”. Sources, binaries, models, raw results and full experiments tables are available at 10.5281/zenodo.6806915.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) STOC, pp. 592–601. ACM, New York (1993). https://doi.org/10.1145/167088.167242
André, É.: What’s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transfer 21(2), 203–219 (2017). https://doi.org/10.1007/s10009-017-0467-0
André, É.: IMITATOR 3: synthesis of timing parameters beyond decidability. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 552–565. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_26
André, É., Arias, J., Petrucci, L., Pol, J.: Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12651, pp. 311–329. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72016-2_17
André, É., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819–836 (2009). https://doi.org/10.1142/S0129054109006905
André, É., Fribourg, L., Soulat, R.: Merge and conquer: state merging in parametric timed automata. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 381–396. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_27
André, É., Lime, D., Markey, N.: Language preservation problems in parametric timed automata. Log. Methods Comput. Sci. 16(1) (2020). https://doi.org/10.23638/LMCS-16(1:5)2020
André, É., Lime, D., Roux, O.H.: Integer-complete synthesis for bounded parametric timed automata. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 7–19. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24537-9_2
André, É., Marinho, D., van de Pol, J.: A benchmarks library for extended parametric timed automata. In: Loulergue, F., Wotawa, F. (eds.) TAP 2021. LNCS, vol. 12740, pp. 39–50. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79379-1_3
André, É., Nguyen, H.G., Petrucci, L.: Efficient parameter synthesis using optimized state exploration strategies. In: Hu, Z., Bai, G. (eds.) ICECCS, pp. 1–10. IEEE (2017). https://doi.org/10.1109/ICECCS.2017.28
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. Program. 72(1–2), 3–21 (2008). https://doi.org/10.1016/j.scico.2007.08.001
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 146–165. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_11
Becchi, A., Zaffanella, E.: PPLite: zero-overhead encoding of NNC polyhedra. Inf. Comput. 275, 1–36 (2020). https://doi.org/10.1016/j.ic.2020.104620
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. Transfer 8(3), 204–215 (2006). https://doi.org/10.1007/s10009-005-0190-0
Ben Salah, R., Bozga, M., Maler, O.: On interleaving in timed automata. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 465–476. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949_31
Bezděk, P., Beneš, N., Barnat, J., Černá, I.: LTL parameter synthesis of parametric timed automata. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 172–187. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_12
Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: Reachability analysis of linear hybrid systems via block decomposition. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 39(11), 4018–4029 (2020). https://doi.org/10.1109/TCAD.2020.3012859
Chen, X., Ábrahám, E., Frehse, G.: Efficient bounded reachability computation for rectangular automata. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 139–152. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24288-5_13
Chen, X., Sankaranarayanan, S., Ábrahám, E.: Under-approximate flowpipes for non-linear continuous systems. In: FMCAD, pp. 59–66. IEEE (2014). https://doi.org/10.1109/FMCAD.2014.6987596
David, A.: Merging DBMs efficiently. In: NWPT, pp. 54–56. DIKU, University of Copenhagen (2005)
Henzinger, T.A.: The theory of hybrid automata. In: Vardi, M.Y., Clarke, E.M. (eds.) LiCS, pp. 278–292. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996.561342
Henzinger, T.A., Manna, Z., Pnueli, A.: Temporal proof methodologies for real-time systems. In: Wise, D.S. (ed.) POPL, pp. 353–366. ACM Press (1991). https://doi.org/10.1145/99583.99629
Herbreteau, F., Srivathsan, B., Tran, T.T., Walukiewicz, I.: Why liveness for timed automata is hard, and what we can do about it. ACM Trans. Comput. Log. 21(3), 17:1–17:28 (2020). https://doi.org/10.1145/3372310
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient emptiness check for timed Büchi automata. Formal Methods Syst. Des. 40(2), 122–146 (2012). https://doi.org/10.1007/s10703-011-0133-1
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 990–1005. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_71
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions for timed automata. Inf. Comput. 251, 67–90 (2016). https://doi.org/10.1016/j.ic.2016.07.004
Herbreteau, F., Tran, T.-T.: Improving search order for reachability testing in timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 124–139. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22975-1_9
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebraic Program. 52–53, 183–220 (2002). https://doi.org/10.1016/S1567-8326(02)00037-1
Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015). https://doi.org/10.1109/TSE.2014.2357445
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). https://doi.org/10.1007/978-3-642-39799-8_69
Nguyen, H.G., Petrucci, L., Van de Pol, J.: Layered and collecting NDFS with subsumption for parametric timed automata. In: Lin, A.W., Sun, J. (eds.) ICECCS, pp. 1–9. IEEE Computer Society, December 2018. https://doi.org/10.1109/ICECCS2018.2018.00009
Schupp, S., Nellen, J., Ábrahám, E.: Divide and conquer: variable set separation in hybrid systems reachability analysis. In: Wiklicky, H., de Vink, E.P. (eds.) QAPL@ETAPS. Electronic Proceedings in Theoretical Computer Science, vol. 250, pp. 1–14 (2017). https://doi.org/10.4204/EPTCS.250.1
Acknowledgements
We thank Benjamin Loillier for helping us testing our artifact. Experiments presented in this paper were carried out using the Grid’5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several universities as well as other organizations (see https://www.grid5000.fr).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Results for All Heuristics on the Full Benchmark
A Results for All Heuristics on the Full Benchmark
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
André, É., Marinho, D., Petrucci, L., van de Pol, J. (2022). Efficient Convex Zone Merging in Parametric Timed Automata. In: Bogomolov, S., Parker, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2022. Lecture Notes in Computer Science, vol 13465. Springer, Cham. https://doi.org/10.1007/978-3-031-15839-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-031-15839-1_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-15838-4
Online ISBN: 978-3-031-15839-1
eBook Packages: Computer ScienceComputer Science (R0)