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
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"
}