Computational techniques for hybrid system verification

doi:10.1109/TAC.2002.806655

Computational techniques for hybrid system verification

2003-01-01

259

OA

AI

DOI：10.1109/TAC.2002.806655

Original

Original request for help

Save

Abstract

En 中文

This paper concerns computational methods for verifying properties of polyhedral invariant hybrid automata (PIHA), which are hybrid automata with discrete transitions governed by polyhedral guards. To verify properties of the state trajectories for PIHA, the planar switching surfaces are partitioned to define a finite set of discrete states in an approximate quotient transition system (AQTS). State transitions in the AQTS are determined by the reachable states, or flow pipes, emitting from the switching surfaces according to the continuous dynamics. This paper presents a method for computing polyhedral approximations to flow pipes. It is shown that the flow-pipe approximation error can be made arbitrarily small for general nonlinear dynamics and that the computations can be made more efficient for affine systems. The paper also describes CheckMate, a MATLAB-based tool for modeling, simulating and verifying properties of hybrid systems based on the computational methods previously described.

Keywords:

hybrid systems

model checking

reachability

verification

Computational techniques for hybrid system verification

Abstract

Journal

Organization