Symbolic Model Checking of Hybrid Systems using Template Polyhedra.Sriram Sankaranarayanan, Franjo Ivancic, and Thao Dang |
|
We propose techniques for the verification of hybrid systems
using template polyhedra, i.e., polyhedra whose inequalities have
fixed expressions but with varying constant terms. Given a hybrid
system description and a set of template linear expressions as inputs,
our technique constructs over-approximations of the reachable states
using template polyhedra. The advantages of using template polyhedra
are that operations used in symbolic model checking such as
intersection, union and post-condition across discrete transitions
over template polyhedra can be computed efficiently without using
expensive vertex enumeration.
Additionally, the verification of hybrid systems requires techniques
to handle the continous dynamics inside locations. A key contribution
of the paper is a new flowpipe construction algorithm using template
polyhedra. Our technique uses higher-order Taylor series
approximations along with repeated optimization problems to bound the
terms in the Taylor series expansion. The location invariant is used
to enclose the remainder term of the Taylor series, and thus make our
technique sound. As a result, we can compute flowpipe segments using
template polyhedra that leads to a precise treatment of the continuous
dynamics. Finally, we have implemented our approach as a part of the
tool TimePass for verifying reachability properties of affine hybrid
automata. |
| ps pdf |
| Tools And Algorithms for Construction and Analysis of Systems (TACAS 2008), Vol. 4963 of Lecture Notes in Computer Science, pages 188-202. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |