MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

MPI-I-1999-2-006

A deductive model checking approach for hybrid systems

Nonnengart, Andreas

November 1999, 40 pages.

.
Status: available - back from printing

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.

  • MPI-I-1999-2-006.ps
  • Attachement: MPI-I-1999-2-006.ps (521 KBytes)

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1999-2-006

Hide details for BibTeXBibTeX
@TECHREPORT{NonnengartMPI-I-1999-2-006,
  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},
}