Publication Details

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

HOLÍK, L., VOJNAR, T., BOUAJJANI, A., HABERMEHL, P., TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008.
Czech title
Testování univerzality stromových automatů založené na protiřetězcích
Type
presentation
Language
English
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Bouajjani Ahmed
Habermehl Peter
Touili Tayssir, Dr., Ph.D.
URL
Keywords

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

Abstract

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.

Published
2008
Pages
15
Publisher
Faculty of Information Technology BUT
Place
FIT-TR-2008-007, Brno
BibTeX 
@misc{BUT63965,
  author="Lukáš {Holík} and Tomáš {Vojnar} and Ahmed {Bouajjani} and Peter {Habermehl} and Tayssir {Touili}",
  title="Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata",
  year="2008",
  pages="15",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2008-007, Brno",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhhtv-nartmc-tr-08.pdf",
  note="presentation"
}
Back to top