×

Pegasus: sound continuous invariant generation. (English) Zbl 1505.68045

Summary: Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
34-04 Software, source code, etc. for problems pertaining to ordinary differential equations
68Q60 Specification and verification (program logics, model checking, etc.)
93B03 Attainable sets, reachability
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Almagor S, Kelmendi E, Ouaknine J, Worrell J (2020) Invariants for continuous linear dynamical systems. In: ICALP, LIPIcs, vol 168, pp 107:1-107:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2020.107
[2] Alur, R.; Henzinger, TA; Lafferriere, G.; Pappas, GJ, Discrete abstractions of hybrid systems, Proc IEEE, 88, 7, 971-984 (2000) · doi:10.1109/5.871304
[3] Arrowsmith, D.; Place, CM, Dynamical systems: differential equations, maps, and chaotic behaviour (1992), Boca Raton: CRC Press, Boca Raton · Zbl 0754.34001 · doi:10.1007/978-94-011-2388-4
[4] Beckert B, Giese M, Hähnle R, Klebanov V, Rümmer P, Schlager S, Schmitt PH (2007) The KeY system 1.0 (deduction component). In: Pfenning F (ed) CADE, LNCS, vol 4603, pp 379-384. Springer. doi:10.1007/978-3-540-73595-3_26
[5] Bellman, R., Vector Lyapunov functions, SIAM J Control Optim, 1, 1, 32-34 (1962) · Zbl 0144.10901 · doi:10.1137/0301003
[6] Ben Sassi MA, Girard A, Sankaranarayanan S (2014) Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: CDC, pp 6348-6353. IEEE. doi:10.1109/CDC.2014.7040384
[7] Bogomolov S, Giacobbe M, Henzinger TA, Kong H (2017) Conic abstractions for hybrid systems. In: Abate A, Geeraerts G (eds) FORMATS, LNCS, vol 10419, pp 116-132. Springer. doi:10.1007/978-3-319-65765-3_7 · Zbl 1497.93109
[8] Böhme S, Weber T (2010) Fast LCF-style proof reconstruction for Z3. In: Kaufmann M, Paulson LC (eds) ITP, LNCS, vol 6172, pp 179-194. Springer. doi:10.1007/978-3-642-14052-5_14 · Zbl 1291.68328
[9] Bohrer B, Fernández M, Platzer A \((2019) dL_\iota \): Definite descriptions in differential dynamic logic. In: Fontaine P (ed) CADE, LNCS, vol 11716, pp 94-110. Springer. doi:10.1007/978-3-030-29436-6_6 · Zbl 07178971
[10] Bohrer, B.; Tan, YK; Mitsch, S.; Myreen, MO; Platzer, A.; Foster, JS; Grossman, D., VeriPhy: verified controller executables from verified cyber-physical system models, PLDI, 617-630 (2018), New York: ACM, New York · doi:10.1145/3192366.3192406
[11] Boreale M (2020) Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs. Science of Computer Programming 193. doi:10.1016/j.scico.2020.102441
[12] Chen, M.; Han, X.; Tang, T.; Wang, S.; Yang, M.; Zhan, N.; Zhao, H.; Zou, L.; Hinchey, MG; Bowen, JP; Olderog, E., MARS: a toolchain for modelling, analysis and verification of hybrid systems, Provably correct systems, NASA monographs in systems and software engineering, 39-58 (2017), Berlin: Springer, Berlin · doi:10.1007/978-3-319-48628-4_3
[13] Chicone, C., Ordinary differential equations with applications (2006), New York: Springer, New York · Zbl 1120.34001 · doi:10.1007/0-387-35794-7
[14] Collins GE (1975) Quantifier elimination for real closed fields by cylindrical algebraic decompostion, LNCS, vol 33, pp 134-183. Springer. doi:10.1007/3-540-07407-4_17 · Zbl 0318.02051
[15] Cox, DA; Little, J.; O’Shea, D., Ideals, varieties, and algorithms (2015), Berlin: Springer, Berlin · Zbl 1335.13001 · doi:10.1007/978-3-319-16721-3
[16] Dai, L.; Gan, T.; Xia, B.; Zhan, N., Barrier certificates revisited, J Symb Comput, 80, 62-86 (2017) · Zbl 1357.68110 · doi:10.1016/j.jsc.2016.07.010
[17] Darboux, JG, Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré, Bull Sci Math, 2, 1, 151-200 (1878) · JFM 10.0214.01
[18] Denman W, Muñoz CA (2014) Automated real proving in PVS via MetiTarski. In: Jones CB, Pihlajasaari P, Sun J (eds) FM, LNCS, vol 8442, pp 194-199. Springer. doi:10.1007/978-3-319-06410-9_14
[19] Djaballah, A.; Chapoutot, A.; Kieffer, M.; Bouissou, O., Construction of parametric barrier functions for dynamical systems using interval analysis, Automatica, 78, 287-296 (2017) · Zbl 1357.93046 · doi:10.1016/j.automatica.2016.12.013
[20] Dutertre B, de Moura LM (2006) A fast linear-arithmetic solver for DPLL(T). In: Ball T, Jones RB (eds) CAV, LNCS, vol 4144, pp 81-94. Springer. doi:10.1007/11817963_11
[21] Falconi, M.; Llibre, J., \(n-1\) independent first integrals for linear differential systems in \({\mathbb{R}}^n\) and \({\mathbb{C}}^n\), Qual Theory Dyn Syst, 4, 2, 233-254 (2004) · Zbl 1090.34002 · doi:10.1007/BF02970860
[22] Ferragut, A.; Giacomini, H., A new algorithm for finding rational first integrals of polynomial vector fields, Qual Theory Dyn Syst, 9, 1-2, 89-99 (2010) · Zbl 1216.34001 · doi:10.1007/s12346-010-0021-x
[23] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan G, Qadeer S (eds) CAV, LNCS, vol 6806, pp 379-395. Springer. doi:10.1007/978-3-642-22110-1_30
[24] Fulton N, Mitsch S, Bohrer B, Platzer A (2017) Bellerophon: tactical theorem proving for hybrid systems. In: Ayala-Rincón M, Muñoz CA (eds) ITP, LNCS, vol 10499, pp 207-224. Springer. doi:10.1007/978-3-319-66107-0_14 · Zbl 1483.68191
[25] Fulton N, Mitsch S, Quesel J, Völp M, Platzer A (2015) KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty AP, Middeldorp A (eds) CADE, LNCS, vol 9195, pp 527-538. Springer. doi:10.1007/978-3-319-21401-6_36 · Zbl 1465.68281
[26] Gan, T.; Chen, M.; Li, Y.; Xia, B.; Zhan, N., Reachability analysis for solvable dynamical systems, IEEE Trans Autom Control, 63, 7, 2003-2018 (2018) · Zbl 1423.93057 · doi:10.1109/TAC.2017.2763785
[27] Ghorbal K, Platzer A (2014) Characterizing algebraic invariants by differential radical invariants. In: Ábrahám E, Havelund K (eds) TACAS, LNCS, vol 8413, pp 279-294. Springer. doi:10.1007/978-3-642-54862-8_19
[28] Ghorbal, K.; Sogokon, A.; Platzer, A., A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets, Comput Lang Syst Struct, 47, 1, 19-43 (2017) · Zbl 1379.68238 · doi:10.1016/j.cl.2015.11.003
[29] Goebel R, Hespanha J, Teel AR, Cai C, Sanfelice R (2004) Hybrid systems: generalized solutions and robust stability. In: NOLCOS, vol 37, pp 1-12. Stuttgart, Germany. doi:10.1016/S1474-6670(17)31194-1
[30] Gorbuzov VN, Pranevich AF (2012) First integrals of ordinary linear differential systems. CoRR arXiv:1201.4141
[31] Goriely A (2001) Integrability and nonintegrability of dynamical systems. World Scientific. doi:10.1142/3846 · Zbl 1002.34001
[32] Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Gupta A, Malik S (eds) CAV, LNCS, vol 5123, pp 190-203. Springer. doi:10.1007/978-3-540-70545-1_18 · Zbl 1155.68437
[33] Haddad, WM; Chellaboina, V., Nonlinear dynamical systems and control: a Lyapunov-based approach (2008), Princeton: Princeton University Press, Princeton · Zbl 1142.34001 · doi:10.1515/9781400841042
[34] Herbrand, J., Recherches sur la théorie de la démonstration (1930), Doctorat d’état: Université de Paris, Faculté des Sciences, Doctorat d’état · JFM 56.0824.02
[35] Immler F, Althoff M, Chen X, Fan C, Frehse G, Kochdumper N, Li Y, Mitra S, Tomar MS, Zamani M (2018) ARCH-COMP18 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse G, Althoff M, Bogomolov S, Johnson TT (eds) ARCH, EPiC series in computing, vol 54. EasyChair, pp 53-70
[36] Kapinski, J.; Deshmukh, JV; Sankaranarayanan, S.; Arechiga, N.; Fränzle, M.; Lygeros, J., Simulation-guided Lyapunov analysis for hybrid dynamical systems, HSCC, 133-142 (2014), New York: ACM, New York · Zbl 1362.93108 · doi:10.1145/2562059.2562139
[37] Kasner, E., Solutions of the Einstein equations involving functions of only one variable, Trans Am Math Soc, 27, 2, 155-162 (1925) · JFM 51.0708.01 · doi:10.1090/S0002-9947-1925-1501305-1
[38] Khalil, HK, Nonlinear systems (1992), New York: Macmillan Publishing Company, New York · Zbl 0969.34001
[39] Kong, H.; Bogomolov, S.; Schilling, C.; Jiang, Y.; Henzinger, TA; Frehse, G.; Mitra, S., Safety verification of nonlinear hybrid systems based on invariant clusters, HSCC, 163-172 (2017), New York: ACM, New York · Zbl 1369.93185 · doi:10.1145/3049797.3049814
[40] Kong H, He F, Song X, Hung WNN, Gu M (2013) Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina N, Veith H (eds) CAV, LNCS, vol 8044, pp 242-257. Springer. doi:10.1007/978-3-642-39799-8_17 · Zbl 1357.68113
[41] Kong S, Gao S, Chen W, Clarke EM (2015) dReach: \( \delta \)-reachability analysis for hybrid systems. In: Baier C, Tinelli C (eds) TACAS, LNCS, vol 9035, pp 200-205. Springer. doi:10.1007/978-3-662-46681-0_15
[42] Lafferriere, G.; Pappas, GJ; Yovine, S., Symbolic reachability computation for families of linear vector fields, J Symb Comput, 32, 3, 231-253 (2001) · Zbl 0983.93004 · doi:10.1006/jsco.2001.0472
[43] Liu J, Lv J, Quan Z, Zhan N, Zhao H, Zhou C, Zou L (2010) A calculus for hybrid CSP. In: Ueda K (ed) APLAS, LNCS, vol 6461, pp 1-15. Springer. doi:10.1007/978-3-642-17164-2_1
[44] Liu, J.; Zhan, N.; Zhao, H.; Chakraborty, S.; Jerraya, A.; Baruah, SK; Fischmeister, S., Computing semi-algebraic invariants for polynomial dynamical systems, EMSOFT, 97-106 (2011), New York: ACM, New York · doi:10.1145/2038642.2038659
[45] Llibre, J.; Zhang, X., Invariant algebraic surfaces of the Lorenz system, J Math Phys, 43, 3, 1622-1645 (2002) · Zbl 1059.34005 · doi:10.1063/1.1435078
[46] Loeser T, Iwasaki Y, Fikes R (1998) Safety verification proofs for physical systems. In: Proc. of the 12th intl. workshop on qualitative reasoning, pp 88-95
[47] Man, Y., Computing closed form solutions of first order ODEs using the Prelle-Singer procedure, J Symb Comput, 16, 5, 423-443 (1993) · Zbl 0793.34002 · doi:10.1006/jsco.1993.1057
[48] Man, Y., First integrals of autonomous systems of differential equations and the Prelle-Singer procedure, J Phys A Math Gen, 27, 10, L329-L332 (1994) · Zbl 0830.34003 · doi:10.1088/0305-4470/27/10/005
[49] Mishra, B., Algorithmic algebra (1993), Berlin: Springer, Berlin · Zbl 0804.13009 · doi:10.1007/978-1-4612-4344-1
[50] Mitsch, S.; Platzer, A., ModelPlex: verified runtime validation of verified cyber-physical system models, Formal Methods Syst Des, 49, 1-2, 33-74 (2016) · Zbl 1380.68282 · doi:10.1007/s10703-016-0241-z
[51] Mitsch, S.; Platzer, A.; Ahrendt, W.; Bubel, R.; Beckert, B.; Hähnle, R.; Ulbrich, M., A retrospective on developing hybrid systems provers in the KeYmaera family: a tale of three provers, Deductive verification: the state of the future, LNCS (2020), Berlin: Springer, Berlin
[52] Olver PJ (2000) Applications of Lie groups to differential equations, graduate texts in mathematics, vol 107, 2nd edn. Springer. doi:10.1007/978-1-4684-0274-2 · Zbl 0937.58026
[53] Papachristodoulou A, Anderson J, Valmorbida G, Prajna S, Seiler P, Parrilo PA (2013) SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB. CoRR arXiv:1310.4716
[54] Papachristodoulou A, Prajna S (2002) On the construction of Lyapunov functions using the sum of squares decomposition. In: CDC, vol 3, pp 3482-3487. doi:10.1109/CDC.2002.1184414
[55] Parrilo PA (2000) Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Ph.D. thesis, California Institute of Technology. doi:10.7907/2K6Y-CH43
[56] Platzer, A., Differential dynamic logic for hybrid systems, J Autom Reason, 41, 2, 143-189 (2008) · Zbl 1181.03035 · doi:10.1007/s10817-008-9103-8
[57] Platzer A (2012) The complete proof theory of hybrid systems. In: LICS, pp 541-550. IEEE Computer Society. doi:10.1109/LICS.2012.64 · Zbl 1364.03045
[58] Platzer A (2012) A differential operator approach to equational differential invariants—(invited paper). In: Beringer L, Felty AP (eds) ITP, LNCS, vol 7406, pp 28-48. Springer. doi:10.1007/978-3-642-32347-8_3 · Zbl 1360.68596
[59] Platzer A (2012) Logics of dynamical systems. In: LICS, pp 13-24. IEEE Computer Society. doi:10.1109/LICS.2012.13 · Zbl 1362.68178
[60] Platzer, A., A complete uniform substitution calculus for differential dynamic logic, J Autom Reason, 59, 2, 219-265 (2017) · Zbl 1437.03119 · doi:10.1007/s10817-016-9385-1
[61] Platzer, A.; Clarke, EM, Computing differential invariants of hybrid systems as fixedpoints, Formal Methods Syst Des, 35, 1, 98-120 (2009) · Zbl 1180.93024 · doi:10.1007/s10703-009-0079-8
[62] Platzer A, Quesel J (2008) KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando A, Baumgartner P, Dowek G (eds) IJCAR, LNCS, vol 5195, pp 171-178. Springer. doi:10.1007/978-3-540-71070-7_15 · Zbl 1165.68469
[63] Platzer A, Quesel J, Rümmer P (2009) Real world verification. In: Schmidt RA (ed) CADE, LNCS, vol 5663, pp 485-501. Springer. doi:10.1007/978-3-642-02959-2_35 · Zbl 1250.68197
[64] Platzer, A.; Tan, YK, Differential equation invariance axiomatization, J ACM, 67, 1 (2020) · Zbl 1494.03079 · doi:10.1145/3380825
[65] Pontryagin, LS, Ordinary differential equations (1962), Oxford: Pergamon Press, Oxford · Zbl 0112.05502 · doi:10.1016/C2013-0-01692-1
[66] Prajna S, Jadbabaie A (2004) Safety verification of hybrid systems using barrier certificates. In: Alur R, Pappas GJ (eds) HSCC, LNCS, vol 2993, pp 477-492. Springer. doi:10.1007/978-3-540-24743-2_32 · Zbl 1135.93317
[67] Prelle, MJ; Singer, MF, Elementary first integrals of differential equations, Trans Am Math Soc, 279, 1, 215-229 (1983) · Zbl 0527.12016 · doi:10.1090/S0002-9947-1983-0704611-X
[68] Rebiha, R.; Moura, AV; Matringe, N., Generating invariants for non-linear hybrid systems, Theor Comput Sci, 594, 180-200 (2015) · Zbl 1328.68130 · doi:10.1016/j.tcs.2015.06.018
[69] Renegar, J.; Goodman, JE; Pollack, R.; Steiger, W., Recent progress on the complexity of the decision problem for the reals, Discrete and computational geometry: papers from the DIMACS special year, 287-308 (1990), New York: DIMACS/AMS, New York · Zbl 0741.03004 · doi:10.1007/978-3-7091-9459-1_11
[70] Rodríguez-Carbonell E, Tiwari A (2005) Generating polynomial invariants for hybrid systems. In: Morari M, Thiele L (eds) HSCC, LNCS, vol 3414, pp 590-605. Springer. doi:10.1007/978-3-540-31954-2_38 · Zbl 1078.93026
[71] Rouche N, Habets P, Laloy M (1977) Stability theory by Liapunov’s direct method, Appl. Math. Sci., vol 22. Springer. doi:10.1007/978-1-4684-9362-7 · Zbl 0364.34022
[72] Roux, P.; Voronin, Y.; Sankaranarayanan, S., Validating numerical semidefinite programming solvers for polynomial invariants, Form Methods Syst Des, 53, 2, 286-312 (2018) · Zbl 1425.68081 · doi:10.1007/s10703-017-0302-y
[73] Roy, MF, Basic algorithms in real algebraic geometry and their complexity: from Sturm’s theorem to the existential theory of reals, De Gruyter Expos Math, 23, 1-67 (1996) · Zbl 0894.14028 · doi:10.1515/9783110811117
[74] Sankaranarayanan, S.; Johansson, KH; Yi, W., Automatic invariant generation for hybrid systems using ideal fixed points, HSCC, 221-230 (2010), New York: ACM, New York · Zbl 1360.34082
[75] Sankaranarayanan S, Chen X, Ábrahám E (2013) Lyapunov function synthesis using Handelman representations. In: NOLCOS, pp 576-581. doi:10.3182/20130904-3-FR-2041.00198
[76] Sankaranarayanan, S.; Sipma, HB; Manna, Z., Constructing invariants for hybrid systems, Form Methods Syst Des, 32, 1, 25-55 (2008) · Zbl 1133.68365 · doi:10.1007/s10703-007-0046-1
[77] Schlomiuk D (1993) Algebraic and geometric aspects of the theory of polynomial vector fields. In: NATO ASI series, vol 408, pp 429-467. Springer, Netherlands. doi:10.1007/978-94-015-8238-4_10 · Zbl 0790.34031
[78] Shi, S., On the nonexistence of rational first integrals for nonlinear systems and semiquasihomogeneous systems, J Math Anal Appl, 335, 1, 125-134 (2007) · Zbl 1132.34004 · doi:10.1016/j.jmaa.2007.01.060
[79] Shults, B.; Kuipers, B., Proving properties of continuous systems: qualitative simulation and temporal logic, Artif Intell, 92, 1-2, 91-129 (1997) · Zbl 1017.68514 · doi:10.1016/S0004-3702(96)00050-1
[80] Slotine, JJE; Li, W., Applied nonlinear control (1991), Upper Saddle River: Prentice-Hall Inc., Upper Saddle River · Zbl 0753.93036
[81] Sogokon A, Ghorbal K, Jackson PB, Platzer A (2016) A method for invariant generation for polynomial continuous systems. In: Jobstmann B, Leino KRM (eds) VMCAI, LNCS, vol 9583, pp 268-288. Springer. doi:10.1007/978-3-662-49122-5_13 · Zbl 1475.68194
[82] Sogokon A, Ghorbal K, Johnson TT (2016) Non-linear continuous systems for safety verification. In: Frehse G, Althoff M (eds) ARCH, EPiC series in computing, vol 43. EasyChair, pp 42-51
[83] Sogokon A, Ghorbal K, Tan YK, Platzer A (2018) Vector barrier certificates and comparison systems. In: Havelund K, Peleska J, Roscoe B, de Vink EP (eds) FM, LNCS, vol 10951, pp 418-437. Springer. doi:10.1007/978-3-319-95582-7_25 · Zbl 1460.93012
[84] Sogokon A, Mitsch S, Tan YK, Cordwell K, Platzer A (2019) Pegasus: a framework for sound continuous invariant generation. In: ter Beek MH, McIver A, Oliveira JN (eds) FM, LNCS, vol 11800, pp 138-157. Springer. doi:10.1007/978-3-030-30942-8_10
[85] Strogatz, SH, Nonlinear dynamics and chaos. Studies in nonlinearity (2001), Boulder: Westview Press, Boulder
[86] Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: Schost É, Emiris IZ (eds) ISSAC, pp 329-336. ACM. doi:10.1145/1993886.1993935 · Zbl 1323.68385
[87] Tiwari A (2003) Approximate reachability for linear systems. In: Maler O, Pnueli A (eds) HSCC, LNCS, vol 2623, pp 514-525. Springer. doi:10.1007/3-540-36580-X_37 · Zbl 1032.93518
[88] Tiwari, A., Abstractions for hybrid systems, Form Methods Syst Des, 32, 1, 57-83 (2008) · Zbl 1133.68368 · doi:10.1007/s10703-007-0044-3
[89] Tiwari A (2008) Generating box invariants. In: Egerstedt M, Mishra B (eds) HSCC, LNCS, vol 4981, pp 658-661. Springer. doi:10.1007/978-3-540-78929-1_58 · Zbl 1144.93311
[90] Tiwari A, Khanna G (2002) Series of abstractions for hybrid automata. In: Tomlin C, Greenstreet MR (eds) HSCC, LNCS, vol 2289, pp 465-478. Springer. doi:10.1007/3-540-45873-5_36 · Zbl 1044.93523
[91] Tiwari A, Khanna G (2004) Nonlinear systems: approximating reach sets. In: Alur R, Pappas GJ (eds) HSCC, LNCS, vol 2993, pp 600-614. Springer. doi:10.1007/978-3-540-24743-2_40 · Zbl 1135.93318
[92] Wang S, Zhan N, Zou L (2015) An improved HHL prover: an interactive theorem prover for hybrid systems. In Butler MJ, Conchon S, Zaïdi F (eds) ICFEM, LNCS, vol 9407, pp 382-399. Springer. doi:10.1007/978-3-319-25423-4_25
[93] Weber, T., Integrating a SAT solver with an LCF-style theorem prover, Electr Notes Theor Comput Sci, 144, 2, 67-78 (2006) · Zbl 1272.68366 · doi:10.1016/j.entcs.2005.12.007
[94] Weber, T., SMT solvers: new oracles for the HOL theorem prover, STTT, 13, 5, 419-429 (2011) · doi:10.1007/s10009-011-0188-8
[95] Yang Z, Huang C, Chen X, Lin W, Liu Z (2016) A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM, LNCS, vol 9995, pp 721-738. doi:10.1007/978-3-319-48989-6_44 · Zbl 1427.68176
[96] Yang, Z.; Wu, M.; Lin, W., An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems, Nonlinear Anal Hybrid Syst, 36, 100837 (2020) · Zbl 07198064 · doi:10.1016/j.nahs.2019.100837
[97] Zaki, MH; Denman, W.; Tahar, S.; Bois, G., Integrating abstraction techniques for formal verification of analog designs, J Aerosp Comput Inf Commun, 6, 5, 373-392 (2009) · doi:10.2514/1.44289
[98] Zhang X (2017) Integrability of dynamical systems: algebra and analysis. Developments in Mathematics, vol 47. Springer. doi:10.1007/978-981-10-4226-3 · Zbl 1373.37053
[99] Zhao, F., Extracting and representing qualitative behaviors of complex systems in phase space, Artif Intell, 69, 1-2, 51-92 (1994) · Zbl 0810.58011 · doi:10.1016/0004-3702(94)90078-7
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.