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

presentation

Language

en

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

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

Keywords

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

Released

03.12.2008

Publisher

Faculty of Information Technology BUT

Location

FIT-TR-2008-007, Brno

Pages count

15

URL

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

Documents

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",
  annote="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.",
  address="Faculty of Information Technology BUT",
  chapter="63965",
  institution="Faculty of Information Technology BUT",
  year="2008",
  month="december",
  publisher="Faculty of Information Technology BUT",
  type="presentation"
}