Symbolic analysis of linear hybrid automata – 25 years later. (English) Zbl 1528.68182
Raskin, Jean-François (ed.) et al., Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 13660, 39-60 (2022).
Summary: We present a collection of advances in the algorithmic verification of hybrid automata with piecewise linear derivatives, so-called Linear Hybrid Automata. New ways to represent and compute with polyhedra, in combination with heuristic algorithmic improvements, have led to considerable speed-ups in checking safety properties through set propagation. We also showcase a CEGAR-style approach that iteratively constructs a polyhedral abstraction. We illustrate the efficiency and scalability of both approaches with two sets of benchmarks.
For the entire collection see [Zbl 1516.68022].
For the entire collection see [Zbl 1516.68022].
MSC:
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Alur, R.: Formal verification of hybrid systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 273-278. ACM (2011) |
| [2] | Alur, R., The algorithmic analysis of hybrid systems, Theor. Comput. Sci., 138, 1, 3-34 (1995) · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T |
| [3] | Alur, R.; Giacobbe, M.; Henzinger, TA; Larsen, KG; Mikučionis, M.; Steffen, B.; Woeginger, G., Continuous-time models for system design and analysis, Computing and Software Science, 452-477 (2019), Cham: Springer, Cham · Zbl 1485.93204 · doi:10.1007/978-3-319-91908-9_22 |
| [4] | Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: IJCAI, pp. 2154-2160. ijcai.org (2021) |
| [5] | Bagnara, R.; Hill, PM; Zaffanella, E., Not necessarily closed convex polyhedra and the double description method, Formal Aspects Comput., 17, 2, 222-257 (2005) · Zbl 1101.68674 · doi:10.1007/s00165-005-0061-1 |
| [6] | 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 |
| [7] | Becchi, A.; Zaffanella, E.; Chockler, H.; Weissenbacher, G., A direct encoding for NNC polyhedra, Computer Aided Verification, 230-248 (2018), Cham: Springer, Cham · Zbl 1511.68069 · doi:10.1007/978-3-319-96145-3_13 |
| [8] | 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 |
| [9] | Becchi, A.; Zaffanella, E.; Chang, B-YE, Revisiting polyhedral analysis for hybrid systems, Static Analysis, 183-202 (2019), Cham: Springer, Cham · Zbl 1539.68149 · doi:10.1007/978-3-030-32304-2_10 |
| [10] | Becchi, A.; Zaffanella, E., PPLite: zero-overhead encoding of NNC polyhedra, Inf. Comput., 275 (2020) · Zbl 1496.68351 · doi:10.1016/j.ic.2020.104620 |
| [11] | Bogomolov, S.; Frehse, G.; Giacobbe, M.; Henzinger, TA; Legay, A.; Margaria, T., Counterexample-guided refinement of template polyhedra, Tools and Algorithms for the Construction and Analysis of Systems, 589-606 (2017), Heidelberg: Springer, Heidelberg · Zbl 1452.68099 · doi:10.1007/978-3-662-54577-5_34 |
| [12] | Boulmé, S., Maréchal, A., Monniaux, D., Périn, M., Yu, H.: The verified polyhedron library: an overview. In: 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2018, Timisoara, Romania, 20-23 September 2018, pp. 9-17. IEEE (2018) |
| [13] | Bu, L., et al.: ARCH-COMP20 category report: hybrid systems with piecewise constant dynamics and bounded model checking. In: ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), Berlin, Germany, 12 July 2020. EPiC Series in Computing, vol. 74, pp. 1-15. EasyChair (2020) |
| [14] | Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: BACH 2 : Bounded reachability checker for compositional linear hybrid systems. In: Design, Automation and Test in Europe, DATE 2010, Dresden, Germany, 8-12 March 2010, pp. 1512-1517 (2010) |
| [15] | Chen, X.; Ábrahám, E.; Moreno-Díaz, R.; Pichler, F.; Quesada-Arencibia, A., Choice of directions for the approximation of reachable sets for hybrid systems, Computer Aided Systems Theory - EUROCAST 2011, 535-542 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-27549-4_69 |
| [16] | Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics 8(6), 282-293 (1968) · Zbl 0218.90030 |
| [17] | Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H.; Emerson, EA; Sistla, AP, Counterexample-guided abstraction refinement, Computer Aided Verification, 154-169 (2000), Heidelberg: Springer, Heidelberg · Zbl 0974.68517 · doi:10.1007/10722167_15 |
| [18] | Clarke, EM; Emerson, EA; Kozen, D., Design and synthesis of synchronization skeletons using branching time temporal logic, Logics of Programs, 52-71 (1982), Heidelberg: Springer, Heidelberg · Zbl 0546.68014 · doi:10.1007/BFb0025774 |
| [19] | Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, New York, NY, USA, pp. 238-252. Association for Computing Machinery (1977) |
| [20] | Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84-96. ACM Press (1978) |
| [21] | Dang, T.; Gawlitza, TM; Yang, H., Template-based unbounded time verification of affine hybrid automata, Programming Languages and Systems, 34-49 (2011), Heidelberg: Springer, Heidelberg · Zbl 1348.68100 · doi:10.1007/978-3-642-25318-8_6 |
| [22] | Frehse, G., PHAVer: algorithmic verification of hybrid systems past HyTech, STTT, 10, 3, 263-279 (2008) · Zbl 1078.93533 · doi:10.1007/s10009-007-0062-x |
| [23] | Frehse, G., et al.: ARCH-COMP19 category report: hybrid systems with piecewise constant dynamics. In: Frehse, G., Althoff, M. (eds.) ARCH19 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol. 61, pp. 1-13. EasyChair (2019) |
| [24] | Frehse, G., et al.: ARCH-COMP18 category report: hybrid systems with piecewise constant dynamics. In: Frehse, G. (eds.) ARCH18 5th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol. 54, pp. 1-13. EasyChair (2018) |
| [25] | Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., Podelski, A.: Eliminating spurious transitions in reachability with support functions. In: Girard, A., Sankaranarayanan, S. (eds.) Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14-16 April 2015, pp. 149-158. ACM (2015) · Zbl 1364.93056 |
| [26] | Frehse, G.; Giacobbe, M.; Henzinger, TA; Chockler, H.; Weissenbacher, G., Space-time interpolants, Computer Aided Verification, 468-486 (2018), Cham: Springer, Cham · Zbl 1511.68155 · doi:10.1007/978-3-319-96145-3_25 |
| [27] | Frehse, G.; Jha, SK; Krogh, BH; Egerstedt, M.; Mishra, B., A counterexample-guided approach to parameter synthesis for linear hybrid automata, Hybrid Systems: Computation and Control, 187-200 (2008), Heidelberg: Springer, Heidelberg · Zbl 1143.68435 · doi:10.1007/978-3-540-78929-1_14 |
| [28] | Frehse, G.; Gopalakrishnan, G.; Qadeer, S., SpaceEx: scalable verification of hybrid systems, Computer Aided Verification, 379-395 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-22110-1_30 |
| [29] | Halbwachs, N.; Merchat, D.; Gonnord, L., Some ways to reduce the space dimension in polyhedra computations, Formal Methods Syst. Des., 29, 1, 79-95 (2006) · Zbl 1105.68107 · doi:10.1007/s10703-006-0013-2 |
| [30] | Halbwachs, N.; Proy, Y-E; Raymond, P.; Le Charlier, B., Verification of linear hybrid systems by means of convex approximations, Static Analysis, 223-237 (1994), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-58485-4_43 |
| [31] | Halbwachs, N.; Proy, Y.; Roumanoff, P., Verification of real-time systems using linear relation analysis, Formal Methods Syst. Des., 11, 2, 157-185 (1997) · doi:10.1023/A:1008678014487 |
| [32] | Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278 (1996) |
| [33] | Henzinger, T.; Ho, P-H; Wong-Toi, H., HyTech: a model checker for hybrid systems, Softw. Tools Technol. Transf., 1, 110-122 (1997) · Zbl 1060.68603 · doi:10.1007/s100090050008 |
| [34] | Henzinger, TA; Ho, P-H; Antsaklis, P.; Kohn, W.; Nerode, A.; Sastry, S., HyTech: the Cornell hybrid technology tool, Hybrid Systems II, 265-293 (1995), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-60472-3_14 |
| [35] | Henzinger, TA; Ho, P-H; Wong-Toi, H., Algorithmic analysis of nonlinear hybrid systems, IEEE Trans. Autom. Control, 43, 540-554 (1998) · Zbl 0918.93019 · doi:10.1109/9.664156 |
| [36] | Henzinger, TA; Kopke, PW; Puri, A.; Varaiya, P., What’s decidable about hybrid automata?, J. Comput. Syst. Sci., 57, 94-124 (1998) · Zbl 0920.68091 · doi:10.1006/jcss.1998.1581 |
| [37] | Jeannet, B.; Miné, A.; Bouajjani, A.; Maler, O., Apron: a library of numerical abstract domains for static analysis, Computer Aided Verification, 661-667 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-02658-4_52 |
| [38] | Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. In: HSCC, pp. 287-300 (2007) · Zbl 1221.93115 |
| [39] | Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250-262 (2010). IFAC World Congress 2008 · Zbl 1201.93018 |
| [40] | Maler, O.: Algorithmic verification of continuous and hybrid systems. In: International Workshop on Verification of Infinite-State System (Infinity) (2013) · Zbl 1464.68210 |
| [41] | Miné, A., The octagon abstract domain, High. Order Symb. Comput., 19, 1, 31-100 (2006) · Zbl 1105.68069 · doi:10.1007/s10990-006-8609-1 |
| [42] | Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Kuhn, H.W., Tucker, A.W. (eds.) Contributions to the Theory of Games - Volume II, no. 28. Annals of Mathematics Studies, pp. 51-73. Princeton University Press, Princeton, New Jersey (1953) · Zbl 0050.14201 |
| [43] | Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: PADL, pp. 245-259 (2007) |
| [44] | Queille, JP; Sifakis, J.; Dezani-Ciancaglini, M.; Montanari, U., Specification and verification of concurrent systems in CESAR, International Symposium on Programming, 337-351 (1982), Heidelberg: Springer, Heidelberg · Zbl 0482.68028 · doi:10.1007/3-540-11494-7_22 |
| [45] | Rockafellar, R.T. : Convex Analysis. Princeton University Press, Princeton (1970) · Zbl 0193.18401 |
| [46] | Roohi, N.; Prabhakar, P.; Viswanathan, M.; Chechik, M.; Raskin, J-F, Hybridization based CEGAR for hybrid automata with affine dynamics, Tools and Algorithms for the Construction and Analysis of Systems, 752-769 (2016), Heidelberg: Springer, Heidelberg · Zbl 1420.68138 · doi:10.1007/978-3-662-49674-9_48 |
| [47] | Sankaranarayanan, S.; Colón, MA; Sipma, H.; Manna, Z.; Emerson, EA; Namjoshi, KS, Efficient strongly relational polyhedral analysis, Verification, Model Checking, and Abstract Interpretation, 111-125 (2005), Heidelberg: Springer, Heidelberg · Zbl 1176.68051 · doi:10.1007/11609773_8 |
| [48] | Sankaranarayanan, S.; Dang, T.; Ivančić, F.; Ramakrishnan, CR; Rehof, J., Symbolic model checking of hybrid systems using template polyhedra, Tools and Algorithms for the Construction and Analysis of Systems, 188-202 (2008), Heidelberg: Springer, Heidelberg · Zbl 1134.68419 · doi:10.1007/978-3-540-78800-3_14 |
| [49] | Sankaranarayanan, S.; Sipma, HB; Manna, Z.; Cousot, R., Scalable analysis of linear systems using mathematical programming, Verification, Model Checking, and Abstract Interpretation, 25-41 (2005), Heidelberg: Springer, Heidelberg · Zbl 1111.68514 · doi:10.1007/978-3-540-30579-8_2 |
| [50] | Singh, G., Püschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18-20 January 2017, pp. 46-59. ACM (2017) · Zbl 1380.68131 |
| [51] | Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, New York (2009). doi:10.1007/978-1-4419-0224-5 · Zbl 1195.93001 |
| [52] | Williams, HP, Fourier’s method of linear programming and its dual, Am. Math. Mon., 93, 9, 681-695 (1986) · Zbl 0618.90065 · doi:10.1080/00029890.1986.11971923 |
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.
