The Causal Graph Revisited for Directed Model Checking

11 years 7 days ago
The Causal Graph Revisited for Directed Model Checking
Directed model checking is a well-established technique to tackle the state explosion problem when the aim is to find error states in large systems. In this approach, the state space traversal is guided through a function that estimates the distance to nearest error states. States with lower estimates are preferably expanded during the search. Obviously, the challenge is to develop distance functions that are efficiently computable on the one hand and as informative as possible on the other hand. In this paper, we introduce the causal graph structure to the context of directed model checking. Based on causal graph analysis, we first adapt a distance estimation function from AI planning to directed model checking. Furthermore, we investigate an abstraction that is guaranteed to preserve error states. The experimental evaluation shows the practical potential of these techniques.
Martin Wehrle, Malte Helmert
Added 25 Nov 2009
Updated 25 Nov 2009
Type Conference
Year 2009
Where SAS
Authors Martin Wehrle, Malte Helmert
Comments (0)