Using a Reachability Algorithm to Check CTL

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching-time logics to be verified in linear time. The seminal work of Kupferman et al. showed that:

1. branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata, representing the model and property under verification, and
2. the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product.

Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accepting and rejecting runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called "state recording" from Schuppan and Biere to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While "state recording" increases the size of the state space, the advantage of our approach lies in the memory savings that BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.

Return to index

Last updated by tbourke at Fri Jul 22 15:11:01 2005 GMT+1000