A method and a tool for automatic veriication of region stability for hybrid systems
Andreas Podelski, Silke Wagner · MPG.PuRe (Max Planck Society) · 2007
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.