Publication Details

Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata

BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In: Implementation and Application of Automata. Lecture Notes in Computer Science, vol. 5148. Berlin: Springer Verlag, 2008, pp. 57-67. ISBN 978-3-540-70843-8.
Czech title
Testování univerzality stromových automatů založené na protiřetězcích
Type
conference paper
Language
english
Authors
Bouajjani Ahmed (UPAR7)
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)
Keywords

unversality, tree automata, antichain, abstract regular tree model checking

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.

Published
2008
Pages
57-67
Proceedings
Implementation and Application of Automata
Series
Lecture Notes in Computer Science
Volume
5148
Conference
13th International Conference on Implementation and Application of Automata -- CIAA'08, San Francisco, California, US
ISBN
978-3-540-70843-8
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX 
@INPROCEEDINGS{FITPUB8672,
   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 = "57--67",
   booktitle = "Implementation and Application of Automata",
   series = "Lecture Notes in Computer Science",
   volume = 5148,
   year = 2008,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-70843-8",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8672"
}
Back to top