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

conference paper

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

tree automata, simulation relation, nondeterministic tree automata, reductionm, language preservation

RIV year

2008

Released

31.03.2008

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-540-78799-0

Book

Tools and Algorithms for the Construction and Analysis of Systems

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

93

Pages to

108

Pages count

16

Documents

BibTex 


@inproceedings{BUT30753,
  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.",
  address="Springer Verlag",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  chapter="30753",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  year="2008",
  month="march",
  pages="93--108",
  publisher="Springer Verlag",
  type="conference paper"
}