Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant

To verify the safety of nonlinear dynamical systems based on inductive invariants, key issues include defining the most complete inductive condition and discovering an inductive invariant that satisfies the specified inductive condition. In this paper, to lay a solid foundation for future research into the safety verification of semi- algebraic dynamical systems, we first establish a formal framework for evaluating the quality of continuous inductive conditions. In addition, we propose a new complete and computable inductive condition for verifying the safety of semi-algebraic dynamical systems. Compared with the existing complete and computable inductive condition, this new inductive condition can be easily adapted to achieve a set of sufficient inductive conditions with different level of conservativeness and computational complexity, which provides us with a means to trade off between the verification power and complexity. These inductive conditions can be solved by quantifier elimination and SMT solvers.

Reachable Set Estimation and Safety Verification of Nonlinear Systems via Iterative Sums of Squares Programming

In this paper,the problems of forward reachable set estimation and safety verification of uncertain nonlinear systems with polynomial dynamics are addressed.First,an iterative sums of squares(SOS)programming approach is developed for reachable set estimation.It characterizes the over-approximations of the forward reachable sets by sub-level sets of time-varying Lyapunovlike functions that satisfy an invariance condition,and formulates the problem of searching for the Lyapunov-like functions as a bilinear SOS program,which can be solved via an iterative algorithm.To make the over-approximation tight,the proposed approach seeks to minimize the volume of the overapproximation set with a desired shape.Then,the reachable set estimation approach is extended for safety verification,via explicitly encoding the safety constraint such that the Lyapunov-like functions guarantee both reaching and avoidance.The efficiency of the presented method is illustrated by some numerical examples.

A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems

To cater for the scenario of coordinated transportation of multiple trucks on the highway,a platoon system for autonomous driving has been extensively explored in the industry.Before such a platoon is deployed,it is necessary to ensure the safety of its driving behavior,whereby each vehicle’s behavior is commanded by the decision-making function whose decision is based on the observed driving scenario.However,there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system.In this paper,we focus on the platoon driving scenario,whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways.We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’cooperative driving behaviors.The existing Multi-Lane Spatial Logic(MLSL)with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective.To cater for the platoon system’s multi-vehicle perspective,we modify the existing abstract model and propose a Multi-Agent Spatial Logic(MASL)that extends MLSL by relative orientation and multi-agent observation.We then utilize a timed automata type supporting MASL formulas to model vehicles’decision controllers for platoon driving.Taking the behavior of a human-driven vehicle(HDV)joining the platoon as a case study,we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.