A deductive model checking approach for hybrid systems

In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. This is done by representing a given verification problem as a second-order predicate logic formula which is to be solved (proved valid) with the help of a second-order quantifier elimination method. In contrast to many ``standard'' model checking approaches the method as described in this paper does not perform a forward or backward reachability analysis. Experiments show that this approach is particularly interesting in cases where a standard reachability analysis would require to travel often through some of the given system locations. In addition, the approach offers possibilities to proceed where ``standard'' reachability analysis approaches do not terminate