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

2. Number - All Departments

MPI-I-2007-2-001

A method and a tool for automatic veriication of region stability for hybrid systems

Podelski, Andreas and Wagner, Silke

January 2007, 46 pages.

.
Status: available - back from printing

We propose a model checking method and tool that integrates state abstraction techniques for the automatic proof of a stability property for hybrid systems called \emph{region stability}. It is based on a new notion of \emph{snapshots} which yield characteristic discretizations of trajectories. We have implemented the tool and applied it to solve a number of verification problems, including the fully automatic stability proof for the break curve behavior of a train system.

  • MPI-I-2007-2-001.pdf
  • Attachement: MPI-I-2007-2-001.pdf (235 KBytes)

URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2007-2-001

Hide details for BibTeXBibTeX
@TECHREPORT{PodelskiWagner2007,
  AUTHOR = {Podelski, Andreas and Wagner, Silke},
  TITLE = {A method and a tool for automatic veriication of region stability 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-2007-2-001},
  MONTH = {January},
  YEAR = {2007},
  ISSN = {0946-011X},
}