×

zbMATH — the first resource for mathematics

Barrier certificates revisited. (English) Zbl 1357.68110
Summary: A barrier certificate can separate the state space of a considered hybrid system (HS) into safe and unsafe parts according to the safety property to be verified. Therefore this notion has been widely used in the verification of HSs. A stronger condition on barrier certificates (BCs) means that fewer BCs can be synthesized, as the expressiveness of synthesized BCs is weaker. On the other hand, synthesizing more expressive BCs normally means higher complexity. H. Kong et al. [Lect. Notes Comput. Sci. 8044, 242–257 (2013; Zbl 1357.68113)] investigated how to relax the condition of BCs while still keeping their convexity so that one can synthesize more expressive BCs efficiently using semi-definite programming (SDP). In this paper, we first discuss how to relax the condition of BCs in a general way, while still keeping their convexity. Thus, one can utilize different weaker conditions flexibly to synthesize different kinds of BCs with more expressiveness efficiently using SDP, which gives more opportunities to verify the considered system. We also show how to combine two functions together to form a combined BC in order to prove a safety property under consideration, whereas neither of them may be a BC separately. In fact, the notion of combined BCs is strictly more expressive than that of BCs, so it further brings more chances to verify a considered system. Another contribution of this paper is to investigate how to avoid the unsoundness of SDP based approaches caused by numerical error through symbolic checking.
Reviewer: Reviewer (Berlin)

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68W30 Symbolic computation and algebraic computation
90C22 Semidefinite programming
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theor. Comput. Sci., 138, 1, 3-34, (1995) · Zbl 0874.68206
[2] Chen, X.; Ábrahám, E.; Sankaranarayanan, S., Flow^⁎: an analyzer for non-linear hybrid systems, (CAV’13, Lect. Notes Comput. Sci., vol. 8044, (2013), Springer), 258-263
[3] Dai, L.; Xia, B.; Zhan, N., Generating non-linear interpolants by semidefinite programming, (CAV’13, Lect. Notes Comput. Sci., vol. 8044, (2013), Springer), 364-380
[4] Eggers, A.; Ramdani, N.; Nedialkov, N.; Fränzle, M., Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods, Softw. Syst. Model., 1-28, (2012)
[5] Gao, S.; Kong, S.; Clarke, E. M., Dreal: an SMT solver for nonlinear theories over the reals, (CADE’13, Lect. Notes Comput. Sci., vol. 7898, (2013), Springer), 208-214 · Zbl 1381.68268
[6] Gulwani, S.; Tiwari, A., Constraint-based approach for analysis of hybrid systems, (CAV’08, Lect. Notes Comput. Sci., vol. 5123, (2008), Springer), 190-203 · Zbl 1155.68437
[7] Han, J.; Jin, Z.; Xia, B., Proving inequalities and solving global optimization problems via simplified CAD projection, (2012), CoRR
[8] Henzinger, T. A.; Ho, P.-H., Algorithmic analysis of nonlinear hybrid systems, (CAV’95, Lect. Notes Comput. Sci., vol. 939, (1995), Springer), 225-238
[9] Jirstrand, M., Invariant sets for a class of hybrid systems, (CDC’98, vol. 4, (1998), IEEE), 3699-3704
[10] Jovanovic, D.; de Moura, L. M., Solving non-linear arithmetic, (IJCAR’12, Lect. Notes Comput. Sci., vol. 7364, (2012), Springer), 339-354 · Zbl 1358.68257
[11] Kong, H.; He, F.; Song, X.; Hung, W.; Gu, M., Exponential-condition-based barrier certificate generation for safety verification of hybrid systems, (CAV’13, Lect. Notes Comput. Sci., vol. 8044, (2013), Springer), 242-257 · Zbl 1357.68113
[12] Kong, H.; Song, X.; Han, D.; Gu, M.; Sun, J., A new barrier certificate for safety verification of hybrid systems, Comput. J., 57, 7, 1033-1045, (2013)
[13] Lafferriere, G.; Pappas, G. J.; Yovine, S., Symbolic reachability computation for families of linear vector fields, J. Symb. Comput., 32, 3, 231-253, (2001) · Zbl 0983.93004
[14] Lin, W.; Wu, M.; Yang, Z.; Zeng, Z., Exact safety verification of hybrid systems using sums-of-squares representation, Sci. China Inf. Sci., 57, 5, 1-13, (2014) · Zbl 1343.93051
[15] Liu, J.; Lv, J.; Quan, Z.; Zhan, N.; Zhao, H.; Zhou, C.; Zou, L., A calculus for hybrid CSP, (APLAS’10, Lect. Notes Comput. Sci., vol. 6461, (2010), Springer), 1-15
[16] Liu, J.; Zhan, N.; Zhao, H., Computing semi-algebraic invariants for polynomial dynamical systems, (EMSOFT’11, (2011), ACM Press), 97-106
[17] Liu, J.; Zhan, N.; Zhao, H.; Zou, L., Abstraction of elementary hybrid systems by variable transformation, (FM’15, Lect. Notes Comput. Sci., vol. 9109, (2015), Springer), 360-377
[18] Parrilo, P. A., Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization, (2000), California Inst. of Tech, PhD thesis
[19] Parrilo, P. A., Semidefinite programming relaxations for semialgebraic problems, Math. Program., 96, 293-320, (2003) · Zbl 1043.14018
[20] Platzer, A.; Clarke, E., Computing differential invariants of hybrid systems as fixedpoints, (CAV’08, Lect. Notes Comput. Sci., vol. 5123, (2008), Springer), 176-189 · Zbl 1155.68445
[21] Platzer, A.; Clarke, E. M., Computing differential invariants of hybrid systems as fixedpoints, Form. Methods Syst. Des., 35, 1, 98-120, (2009) · Zbl 1180.93024
[22] Prajna, S.; Jadbabaie, A., Safety verification of hybrid systems using barrier certificates, (HSCC’04, Lect. Notes Comput. Sci., vol. 2993, (2004), Springer), 477-492 · Zbl 1135.93317
[23] Prajna, S.; Jadbabaie, A.; Pappas, G. J., A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Trans. Autom. Control, 52, 8, 1415-1428, (2007) · Zbl 1366.93711
[24] Prajna, S.; Papachristodoulou, A.; Seiler, P.; Parrilo, P. A., Sostools and its control applications, (Positive Polynomials in Control, (2005), Springer), 273-292 · Zbl 1119.93302
[25] Puri, A.; Varaiya, P., Decidability of hybrid systems with rectangular differential inclusions, (CAV’94, Lect. Notes Comput. Sci., vol. 818, (1994), Springer), 95-104
[26] Ratschan, S.; She, Z., Safety verification of hybrid systems by constraint propagation-based abstraction refinement, ACM Trans. Embed. Comput. Syst., 6, 1, (2007)
[27] Rodríguez-Carbonell, E.; Tiwari, A., Generating polynomial invariants for hybrid systems, (HSCC’05, Lect. Notes Comput. Sci., vol. 3414, (2005), Springer), 590-605 · Zbl 1078.93026
[28] Sankaranarayanan, S., Automatic invariant generation for hybrid systems using ideal fixed points, (HSCC’10, (2010), ACM Press), 221-230 · Zbl 1360.34082
[29] Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Constructing invariants for hybrid systems, (HSCC’04, Lect. Notes Comput. Sci., vol. 2993, (2004), Springer), 539-554 · Zbl 1135.93322
[30] Sloth, C.; Pappas, G. J.; Wisniewski, R., Compositional safety analysis using barrier certificates, (HSCC’12, (2012), ACM Press), 15-24 · Zbl 1362.68185
[31] Taly, A.; Tiwari, A., Deductive verification of continuous dynamical systems, (FSTTCS’09, LIPIcs, vol. 4, (2009)), 383-394 · Zbl 1248.68336
[32] Wu, M.; Yang, Z., Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients, (SNC’11, (2011), ACM), 104-111 · Zbl 1345.65046
[33] Yang, Z.; Lin, W.; Wu, M., Exact safety verification of hybrid systems based on bilinear SOS representation, ACM Trans. Embed. Comput. Syst., 14, 1, 16:1-16:19, (2015)
[34] Zhan, N.; Wang, S.; Zhao, H., Formal modelling, analysis and verification of hybrid systems, (Unifying Theories of Programming and Formal Engineering Methods, Lect. Notes Comput. Sci., vol. 8050, (2013), Springer), 207-281 · Zbl 1444.68105
[35] Zhao, H.; Yang, M.; Zhan, N.; Gu, B.; Zou, L.; Chen, Y., Formal verification of a descent guidance control program of a lunar lander, (FM’14, Lect. Notes Comput. Sci., vol. 8442, (2014), Springer), 733-748
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.