Technical report

BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008.
Publication language:english
Original title:Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
Title (cs):Testování univerzality stromových automatů založené na protiřetězcích
Pages:15
Place:FIT-TR-2008-007, Brno, CZ
Year:2008
Publisher:Faculty of Information Technology BUT
URL:http://www.fit.vutbr.cz/~vojnar/Publications/bhhtv-nartmc-tr-08.pdf [PDF]
Keywords
universality, tree automata, antichain, abstract regular tree model checking
Annotation
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.
BibTeX:
@TECHREPORT{
   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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=8818}
}

Your IPv4 address: 54.158.55.5
Switch to IPv6 connection

DNSSEC [dnssec]