Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


A deductive model checking approach for hybrid systems

Nonnengart, Andreas

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
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.

References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-1999-2-006.ps521 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Nonnengart, Andreas},
  TITLE = {A deductive model checking approach for hybrid systems},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-1999-2-006},
  MONTH = {November},
  YEAR = {1999},
  ISSN = {0946-011X},