2008 | OriginalPaper | Chapter
Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
Authors : Ahmed Bouajjani, Peter Habermehl, Lukáš Holík, Tayssir Touili, Tomáš Vojnar
Published in: Implementation and Applications of Automata
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.