非表示:
キーワード:
-
要旨:
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.
