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 Bouajjani | 1 | 2663 | 184.84 |
Peter Habermehl | 2 | 502 | 30.39 |
Lukáš Holík | 3 | 157 | 6.67 |
Tayssir Touili | 4 | 758 | 47.21 |
Tomáš Vojnar | 5 | 533 | 32.06 |