Uppaal/DMC is an extension of UPPAAL which provides generic heuristics for directed model checking. In this approach, the traversal of the state space is guided by a heuristic function which estimates the distance of a search state to the nearest error state. Our tool combines two recent approaches to design such estimation functions. Both are based on computing an abstraction of the system and using the error distance in this abstraction as the heuristic value. The abstractions, and thus the heuristic functions, are generated fully automatically and do not need any additional user input. UPPAAL/DMC needs less time and memory to find shorter error paths than UPPAAL'S standard search methods. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Kupferschmid, S., Dräger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., & Behrmann, G. (2007). Uppaal/DMC - Abstraction-based heuristics for directed model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4424 LNCS, pp. 679–682). Springer Verlag. https://doi.org/10.1007/978-3-540-71209-1_52
Mendeley helps you to discover research relevant for your work.