Detail publikace

Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata

HOLÍK, L. VOJNAR, T. ABDULLA, P. BOUAJJANI, A. KAATI, L.

Originální název

Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata

Typ

zpráva odborná

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

finite tree automata, simulation, size reduction, combination of simulation relations

Autoři

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L.

Vydáno

9. 6. 2008

Místo

FIT-TR-2008-001, Brno

Strany počet

34

URL

http://www.fit.vutbr.cz/~vojnar/Publications/abhkv-simtree-tr-07.pdf

BibTex

@techreport{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",
  year="2008",
  address="FIT-TR-2008-001, Brno",
  pages="34",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/abhkv-simtree-tr-07.pdf"
}