Help Privacy Policy Disclaimer
  Advanced SearchBrowse





A deductive model checking approach for hybrid systems


Nonnengart,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Any fulltext), 429KB

Supplementary Material (public)
There is no public supplementary material available

Nonnengart, A.(1999). A deductive model checking approach for hybrid systems (MPI-I-1999-2-006). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-6F5B-0
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.