max planck institut
informatik
informatik
MPI-I-1999-2-006. November 1999, 40 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:
| To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
|---|---|
| 521 KBytes | |
| Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView | |
BibTeX