Publication Details
Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
Habermehl Peter (UPAR7)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Touili Tayssir (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
universality, tree automata, antichain, abstract regular tree model checking
This report provides the full version of a CIAA'08 paper, in which we propose a 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.
@TECHREPORT{FITPUB8818,
author = "Ahmed Bouajjani and Peter Habermehl and Luk\'{a}\v{s} Hol\'{i}k and Tayssir Touili and Tom\'{a}\v{s} Vojnar",
title = "Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata",
pages = 15,
year = 2008,
location = "FIT-TR-2008-007, Brno, CZ",
publisher = "Faculty of Information Technology BUT",
language = "english",
url = "https://www.fit.vut.cz/research/publication/8818"
}