Title
Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
Abstract
We propose new antichain-based algorithms for checking universality and inclusion of nondeterministic tree automata (NTA). We have implemented these algorithms in a prototype tool and our experiments show that they provide a significant improvement over the traditional determinisation-based approaches. We use our antichain-based inclusion checking algorithm to build an abstract regular tree model checking framework based entirely on NTA. We show the significantly improved efficiency of this framework through a series of experiments with verifying various programs over dynamic linked tree-shaped data structures.
Year
DOI
Venue
2008
10.1007/978-3-540-70844-5_7
CIAA
Keywords
Field
DocType
nondeterministic finite tree automata,antichain-based inclusion checking algorithm,antichain-based universality,tree-shaped data structure,new antichain-based algorithm,checking framework,traditional determinisation-based approach,improved efficiency,abstract regular tree model,significant improvement,inclusion testing,prototype tool,nondeterministic tree automaton,model checking,data structure
Discrete mathematics,Data structure,Antichain,Nondeterministic algorithm,Automaton,Decision tree model,Theoretical computer science,Universality (philosophy),Mathematics
Conference
Volume
ISSN
Citations 
5148
0302-9743
14
PageRank 
References 
Authors
0.76
7
5
Name
Order
Citations
PageRank
Ahmed Bouajjani12663184.84
Peter Habermehl250230.39
Lukáš Holík31576.67
Tayssir Touili475847.21
Tomáš Vojnar553332.06