Publication detail

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

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

Original Title

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

English Title

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

Type

conference paper

Language

en

Original 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.

English 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.

Keywords

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

RIV year

2008

Released

18.08.2008

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-540-70843-8

Book

Implementation and Application of Automata

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

57

Pages to

67

Pages count

11

Documents

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",
  annote="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.",
  address="Springer Verlag",
  booktitle="Implementation and Application of Automata",
  chapter="34275",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  year="2008",
  month="august",
  pages="57--67",
  publisher="Springer Verlag",
  type="conference paper"
}