Safety Verification of Discrete-Time Systems via Interpolation-Inspired Barrier Certificates

被引：0

作者：

University of Colorado, Department of Computer Science, Boulder ^{[1
]}

80309, United States

机构：

[1] University of Colorado, Department of Computer Science, Boulder, 80309, CO

来源：

IEEE Control Syst. Lett. | / 3183-3188期

基金：

美国国家科学基金会;

关键词：

barrier certificates; Hybrid systems; interpolation; safety;

D O I：

10.1109/LCSYS.2024.3521356

中图分类号：

学科分类号：

摘要：

Barrier certificates provide an effective automated approach to verifying the safety of dynamical systems. A barrier certificate is a real-valued function over states of the system whose zero level set separates the unsafe region from all possible trajectories starting from a given set of initial states. Typically, the system dynamics must be nonincreasing in the value of the barrier certificate with each transition. Thus, the states of the system that are nonpositive with respect to the barrier certificate act as an over-approximation of the reachable states. The search for such certificates is typically automated by first fixing a template of functions and then using optimization and satisfiability modulo theory (SMT) solvers to find them. Unfortunately, it may not be possible to find a single function in this fixed template. To tackle this challenge, we propose the notion of interpolation-inspired barrier certificate. Instead of a single function, an interpolation-inspired barrier certificate consists of a set of functions such that the union of their sublevel sets over-approximate the reachable set of states. We show how one may find interpolation-inspired barrier certificates of a fixed template, even when we fail to find standard barrier certificates of the same template. We present sum-of-squares (SOS) programming as a computational method to find this set of functions and demonstrate effectiveness of this method over a case study. © 2017 IEEE.

引用

页码：3183 / 3188

页数：5

共 17 条

[1]

Prajna S., Jadbabaie A., Safety verification of hybrid systems using barrier certificates, Proc. Int. Workshop Hybrid Syst. Comput. Control, pp. 477-492, (2004)

[2]

Parrilo P.A., Semidefinite programming relaxations for semialgebraic problems, Math. Program., 96, pp. 293-320, (2003)

[3]

De Moura L., Bjorner N., Satisfiability modulo theories: Introduction and applications, Commun. ACM, 54, 9, pp. 69-77, (2011)

[4]

McMillan K.L., Interpolation and SAT-based model checking, Proc. 15th Int. Conf. Comput. Aided Verification, pp. 1-13, (2003)

[5]

Cormen T.H., Leiserson C.E., Rivest R.L., Stein C., Introduction to Algorithms, (2022)

[6]

Cabodi G., Nocco S., Quer S., Strengthening model checking techniques with inductive invariants, IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., 28, 1, pp. 154-158, (2009)

[7]

Zhang L., Prasad M.R., Hsiao M.S., Incremental deductive & inductive reasoning for SAT-based bounded model checking, Proc. IEEE/ACM Int. Conf. Comput. Aided Design, pp. 502-509, (2004)

[8]

Bradley A.R., SAT-based model checking without unrolling, Proc. Int. Workshop Verification, Model Checking, Abstract Interpretation, pp. 70-87, (2011)

[9]

Bradley A.R., Understanding IC3, Proc. Int. Conf. Theory Appl. Satisfiability Testing, pp. 1-14, (2012)

[10]

Barry A.J., Majumdar A., Tedrake R., Safety verification of reactive controllers for UAV flight in cluttered environments using barrier certificates, Proc. IEEE Int. Conf. Robot. Autom., pp. 484-490, (2012)

← 1 2 →