TY - GEN
T1 - Abstraction-based guided search for hybrid systems
AU - Bogomolov, Sergiy
AU - Donzé, Alexandre
AU - Frehse, Goran
AU - Grosu, Radu
AU - Johnson, Taylor T.
AU - Ladan, Hamed
AU - Podelski, Andreas
AU - Wehrle, Martin
PY - 2013
Y1 - 2013
N2 - 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 (the region 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 path in the region space. A recent approach in this direction is based on guided 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, an abstraction-based cost function based on pattern databases for guiding the reachability analysis is proposed. 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.
AB - 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 (the region 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 path in the region space. A recent approach in this direction is based on guided 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, an abstraction-based cost function based on pattern databases for guiding the reachability analysis is proposed. 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.
UR - http://www.scopus.com/inward/record.url?scp=84884911560&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39176-7_8
DO - 10.1007/978-3-642-39176-7_8
M3 - Conference contribution
AN - SCOPUS:84884911560
SN - 9783642391750
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 117
EP - 134
BT - Model Checking Software - 20th International Symposium, SPIN 2013, Proceedings
PB - Springer Verlag
T2 - 20th International Symposium on Model Checking Software, SPIN 2013
Y2 - 8 July 2013 through 9 July 2013
ER -