title: Guided search for hybrid systems based on coarse-grained space abstractions.
abstract: Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (theregion space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based onguided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based oncoarse-grained space abstractionsfor guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.
authors.affiliation: IST Austria, Klosterneuburg, Austria ; University of Freiburg, Freiburg, Germany.
authors.forename: Sergiy
authors.initials: S
authors.lastname: Bogomolov
authors.affiliation: University of California, Berkeley, USA.
authors.forename: Alexandre
authors.initials: A
authors.lastname: Donzé
authors.affiliation: Université Joseph Fourier Grenoble 1 - Verimag, Grenoble, France.
authors.forename: Goran
authors.initials: G
authors.lastname: Frehse
authors.affiliation: Vienna University of Technology, Vienna, Austria.
authors.forename: Radu
authors.initials: R
authors.lastname: Grosu
authors.affiliation: University of Texas at Arlington, Arlington, USA.
authors.forename: Taylor T
authors.initials: TT
authors.lastname: Johnson
authors.affiliation: University of Freiburg, Freiburg, Germany.
authors.forename: Hamed
authors.initials: H
authors.lastname: Ladan
authors.affiliation: University of Freiburg, Freiburg, Germany.
authors.forename: Andreas
authors.initials: A
authors.lastname: Podelski
authors.affiliation: University of Basel, Basel, Switzerland.
authors.forename: Martin
authors.initials: M
authors.lastname: Wehrle
keywords: Guided search; Heuristics; Hybrid system; Pattern databases; Reachability analysis