Detail publikace

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

HOLÍK, L. VOJNAR, T. BOUAJJANI, A. HABERMEHL, P. TOUILI, T.

Originální název

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

Typ

zpráva odborná

Jazyk

angličtina

Originální abstrakt

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 showthe significantly improved efficiency of this  framework through aseries of experiments with verifying various programs over dynamiclinked tree-shaped data structures.

Klíčová slova

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

Autoři

HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T.

Vydáno

3. 12. 2008

Nakladatel

Faculty of Information Technology BUT

Místo

FIT-TR-2008-007, Brno

Strany počet

15

URL

http://www.fit.vutbr.cz/~vojnar/Publications/bhhtv-nartmc-tr-08.pdf

BibTex

@techreport{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",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2008-007, Brno",
  pages="15",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhhtv-nartmc-tr-08.pdf"
}