Publication detail
Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata
HOLÍK, L., VOJNAR, T., ABDULLA, P., BOUAJJANI, A., KAATI, L.
Original Title
Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata
English Title
Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata
Type
presentation
Language
en
Original Abstract
We address the problem of computing simulation relations over tree
automata. In particular, we consider downward and upward simulations on
tree automata, which are, loosely speaking, analogous to forward and
backward relations over word automata. We provide simple and efficient
algorithms for computing these relations based on a reduction to the
problem of computing simulations on labelled transition systems.
Furthermore, we show that downward and upward relations can be combined
to get relations compatible with the tree language equivalence, which
can subsequently be used for an efficient size reduction of
nondeterministic tree automata. This is of a very high interest, for
instance, for symbolic verification methods such as regular model
checking, which use tree automata to represent infinite sets of
reachable configurations. We provide experimental results showing the
efficiency of our algorithms on examples of tree automata taken from
regular model checking computations.
English abstract
We address the problem of computing simulation relations over tree
automata. In particular, we consider downward and upward simulations on
tree automata, which are, loosely speaking, analogous to forward and
backward relations over word automata. We provide simple and efficient
algorithms for computing these relations based on a reduction to the
problem of computing simulations on labelled transition systems.
Furthermore, we show that downward and upward relations can be combined
to get relations compatible with the tree language equivalence, which
can subsequently be used for an efficient size reduction of
nondeterministic tree automata. This is of a very high interest, for
instance, for symbolic verification methods such as regular model
checking, which use tree automata to represent infinite sets of
reachable configurations. We provide experimental results showing the
efficiency of our algorithms on examples of tree automata taken from
regular model checking computations.
Keywords
finite tree automata, simulation, size reduction, combination of simulation relations
Released
09.06.2008
Location
FIT-TR-2008-001, Brno
Pages count
34
URL
Documents
BibTex
@misc{BUT63912,
author="Lukáš {Holík} and Tomáš {Vojnar} and Parosh {Abdulla} and Ahmed {Bouajjani} and Lisa {Kaati}",
title="Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata",
annote="We address the problem of computing simulation relations over tree
automata. In particular, we consider downward and upward simulations on
tree automata, which are, loosely speaking, analogous to forward and
backward relations over word automata. We provide simple and efficient
algorithms for computing these relations based on a reduction to the
problem of computing simulations on labelled transition systems.
Furthermore, we show that downward and upward relations can be combined
to get relations compatible with the tree language equivalence, which
can subsequently be used for an efficient size reduction of
nondeterministic tree automata. This is of a very high interest, for
instance, for symbolic verification methods such as regular model
checking, which use tree automata to represent infinite sets of
reachable configurations. We provide experimental results showing the
efficiency of our algorithms on examples of tree automata taken from
regular model checking computations.
",
chapter="63912",
year="2008",
month="june",
type="presentation"
}