Paper Info
Title
Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis
Abstract
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. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312-360, 2000] 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 accept and reject 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 [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2-3):185-204, 2004] 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 saving 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.
Year
DOI
Venue
2006
10.1016/j.entcs.2005.07.025
Electr. Notes Theor. Comput. Sci.
Keywords
DocType
Volume
bdd-based approach,alternating tree automata,product automaton,finite state model checking,solution graph,and/or graph,reachability analysis,explicit-state model checker,model checking,state recording,branching-time model checking,state space,symbolic reachability analysis,explicit-state model checking,language emptiness checking,linear time
Journal
149
Issue
ISSN
Citations 
2
Electronic Notes in Theoretical Computer Science
2
PageRank 
References 
Authors
0.39
18
2
Name
Order
Citations
PageRank
Kairong Qian1633.38
Albert Nymeyer21069.98