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

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Rok RIV

2008

Vydáno

18. 8. 2008

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-70843-8

Kniha

Implementation and Application of Automata

Edice

Lecture Notes in Computer Science

Strany od

57

Strany do

67

Strany počet

11

BibTex

@inproceedings{BUT34275,
  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",
  booktitle="Implementation and Application of Automata",
  year="2008",
  series="Lecture Notes in Computer Science",
  volume="5148",
  pages="57--67",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-70843-8"
}