Efficient convex zone merging in parametric timed automata. (English) Zbl 07643436
Bogomolov, Sergiy (ed.) et al., Formal modeling and analysis of timed systems. 20th international conference, FORMATS 2022, Warsaw, Poland, September 13–15, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13465, 200-218 (2022).
Summary: 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.
For the entire collection see [Zbl 1503.68012].
For the entire collection see [Zbl 1503.68012].
MSC:
| 68Qxx | Theory of computing |
References:
| [1] | Alur, R.; Dill, DL, A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8 |
| [2] | 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). doi:10.1145/167088.167242 · Zbl 1310.68139 |
| [3] | André, É., What’s decidable about parametric timed automata?, Int. J. Softw. Tools Technol. Transfer, 21, 2, 203-219 (2017) · doi:10.1007/s10009-017-0467-0 |
| [4] | André, É.; Silva, A.; Leino, KRM, IMITATOR 3: synthesis of timing parameters beyond decidability, Computer Aided Verification, 552-565 (2021), Cham: Springer, Cham · Zbl 1493.68202 · doi:10.1007/978-3-030-81685-8_26 |
| [5] | André, É.; Arias, J.; Petrucci, L.; Pol, J.; Groote, JF; Larsen, KG, Iterative bounded synthesis for efficient cycle detection in parametric timed automata, Tools and Algorithms for the Construction and Analysis of Systems, 311-329 (2021), Cham: Springer, Cham · Zbl 1467.68078 · doi:10.1007/978-3-030-72016-2_17 |
| [6] | André, É.; Chatain, T.; Encrenaz, E.; Fribourg, L., An inverse method for parametric timed automata, Int. J. Found. Comput. Sci., 20, 5, 819-836 (2009) · Zbl 1187.68286 · doi:10.1142/S0129054109006905 |
| [7] | André, É.; Fribourg, L.; Soulat, R.; Van Hung, D.; Ogawa, M., Merge and conquer: state merging in parametric timed automata, Automated Technology for Verification and Analysis, 381-396 (2013), Cham: Springer, Cham · Zbl 1410.68194 · doi:10.1007/978-3-319-02444-8_27 |
| [8] | André, É., Lime, D., Markey, N.: Language preservation problems in parametric timed automata. Log. Methods Comput. Sci. 16(1) (2020). doi:10.23638/LMCS-16(1:5)2020 · Zbl 1429.68098 |
| [9] | André, É.; Lime, D.; Roux, OH; Bojańczyk, M.; Lasota, S.; Potapov, I., Integer-complete synthesis for bounded parametric timed automata, Reachability Problems, 7-19 (2015), Cham: Springer, Cham · Zbl 1471.68111 · doi:10.1007/978-3-319-24537-9_2 |
| [10] | André, É.; Marinho, D.; van de Pol, J.; Loulergue, F.; Wotawa, F., A benchmarks library for extended parametric timed automata, Tests and Proofs, 39-50 (2021), Cham: Springer, Cham · doi:10.1007/978-3-030-79379-1_3 |
| [11] | 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). doi:10.1109/ICECCS.2017.28 |
| [12] | Bagnara, R.; Hill, PM; 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) · doi:10.1016/j.scico.2007.08.001 |
| [13] | Baier, C.; Katoen, JP, Principles of Model Checking (2008), Cambridge: MIT Press, Cambridge · Zbl 1179.68076 |
| [14] | Becchi, A.; Zaffanella, E.; Podelski, A., An efficient abstract domain for not necessarily closed polyhedra, Static Analysis, 146-165 (2018), Cham: Springer, Cham · Zbl 1511.68070 · doi:10.1007/978-3-319-99725-4_11 |
| [15] | Becchi, A.; Zaffanella, E., PPLite: zero-overhead encoding of NNC polyhedra, Inf. Comput., 275, 1-36 (2020) · Zbl 1496.68351 · doi:10.1016/j.ic.2020.104620 |
| [16] | Behrmann, G.; Bouyer, P.; Larsen, KG; 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) · Zbl 1126.68453 · doi:10.1007/s10009-005-0190-0 |
| [17] | Ben Salah, R.; Bozga, M.; Maler, O.; Baier, C.; Hermanns, H., On interleaving in timed automata, CONCUR 2006 - Concurrency Theory, 465-476 (2006), Heidelberg: Springer, Heidelberg · Zbl 1151.68457 · doi:10.1007/11817949_31 |
| [18] | Bezděk, P.; Beneš, N.; Barnat, J.; Černá, I.; De Nicola, R.; Kühn, E., LTL parameter synthesis of parametric timed automata, Software Engineering and Formal Methods, 172-187 (2016), Cham: Springer, Cham · Zbl 1390.68422 · doi:10.1007/978-3-319-41591-8_12 |
| [19] | 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) · doi:10.1109/TCAD.2020.3012859 |
| [20] | Chen, X.; Ábrahám, E.; Frehse, G.; Delzanno, G.; Potapov, I., Efficient bounded reachability computation for rectangular automata, Reachability Problems, 139-152 (2011), Heidelberg: Springer, Heidelberg · Zbl 1348.68097 · doi:10.1007/978-3-642-24288-5_13 |
| [21] | Chen, X., Sankaranarayanan, S., Ábrahám, E.: Under-approximate flowpipes for non-linear continuous systems. In: FMCAD, pp. 59-66. IEEE (2014). doi:10.1109/FMCAD.2014.6987596 |
| [22] | David, A.: Merging DBMs efficiently. In: NWPT, pp. 54-56. DIKU, University of Copenhagen (2005) |
| [23] | Henzinger, T.A.: The theory of hybrid automata. In: Vardi, M.Y., Clarke, E.M. (eds.) LiCS, pp. 278-292. IEEE Computer Society (1996). doi:10.1109/LICS.1996.561342 · Zbl 0959.68073 |
| [24] | 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). doi:10.1145/99583.99629 |
| [25] | 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). doi:10.1145/3372310 · Zbl 1446.68068 |
| [26] | Herbreteau, F.; Srivathsan, B.; Walukiewicz, I., Efficient emptiness check for timed Büchi automata, Formal Methods Syst. Des., 40, 2, 122-146 (2012) · Zbl 1247.68143 · doi:10.1007/s10703-011-0133-1 |
| [27] | Herbreteau, F.; Srivathsan, B.; Walukiewicz, I.; Sharygina, N.; Veith, H., Lazy abstractions for timed automata, Computer Aided Verification, 990-1005 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_71 |
| [28] | Herbreteau, F.; Srivathsan, B.; Walukiewicz, I., Better abstractions for timed automata, Inf. Comput., 251, 67-90 (2016) · Zbl 1353.68166 · doi:10.1016/j.ic.2016.07.004 |
| [29] | Herbreteau, F.; Tran, T-T; Sankaranarayanan, S.; Vicario, E., Improving search order for reachability testing in timed automata, Formal Modeling and Analysis of Timed Systems, 124-139 (2015), Cham: Springer, Cham · Zbl 1465.68148 · doi:10.1007/978-3-319-22975-1_9 |
| [30] | Hune, T.; Romijn, J.; Stoelinga, M.; Vaandrager, FW, Linear parametric model checking of timed automata, J. Log. Algebraic Program., 52-53, 183-220 (2002) · Zbl 1008.68069 · doi:10.1016/S1567-8326(02)00037-1 |
| [31] | Jovanović, A.; Lime, D.; Roux, OH, Integer parameter synthesis for real-time systems, IEEE Trans. Softw. Eng., 41, 5, 445-461 (2015) · doi:10.1109/TSE.2014.2357445 |
| [32] | Laarman, A.; Olesen, MC; Dalsgaard, AE; Larsen, KG; van de Pol, J.; Sharygina, N.; Veith, H., Multi-core emptiness checking of timed Büchi automata using inclusion abstraction, Computer Aided Verification, 968-983 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_69 |
| [33] | 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. doi:10.1109/ICECCS2018.2018.00009 |
| [34] | 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). doi:10.4204/EPTCS.250.1 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
