Publication detail

Simulations and Aintichains for Efficient Handling of Tree Automata

HOLÍK, L. VOJNAR, T.

Original Title

Simulations and Aintichains for Efficient Handling of Tree Automata

English Title

Simulations and Aintichains for Efficient Handling of Tree Automata

Type

book

Language

en

Original Abstract

This work is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulationbased inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.

English abstract

This work is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulationbased inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.

Keywords

finite automata, finite tree automata, alternating Büchi automata, nondeterminism, simulation, bisimulation, universality, language inclusion, antichain, quotienting, regular tree model checking

RIV year

2010

Released

31.12.2010

Publisher

Faculty of Information Technology BUT

Location

Brno

ISBN

978-80-214-4217-7

Edition

FIT Monograph

Edition number

NEUVEDEN

Pages count

150

BibTex


@book{BUT61288,
  author="Lukáš {Holík} and Tomáš {Vojnar}",
  title="Simulations and Aintichains for Efficient Handling of Tree Automata",
  annote="This work is focused on techniques for finite automata and their use in practice,
with the main emphasis on nondeterministic tree automata. This concerns namely
techniques for size reduction and language inclusion testing, which are two
problems that are crucial for many applications of tree automata. For size
reduction of tree automata, we adapt the simulation quotient technique that is
well established for finite word automata. We give efficient algorithms for
computing tree automata simulations and we also introduce a new type of relation
that arises from a combination of tree automata downward and upward simulation
and that is very well suited for quotienting. The combination principle is
relevant also for word automata. We then generalise the so called antichain
universality and language inclusion checking technique developed originally for
finite word automata for tree automata. Subsequently, we improve the antichain
technique for both word and tree automata by combining it with the
simulationbased inclusion checking techniques, significantly improving efficiency
of the antichain method. We then show how the developed reduction and inclusion
checking methods improve the method of abstract regular tree model checking, the
method that was the original motivation for starting the work on tree automata.
Both the reduction and the language inclusion methods are based on relatively
simple and general principles that can be further extended for other types of
automata and related formalisms. An example is our adaptation of the reduction
methods for alternating Büchi automata, which results in an efficient alternating
automata size reduction technique.",
  address="Faculty of Information Technology BUT",
  chapter="61288",
  edition="FIT Monograph",
  howpublished="print",
  institution="Faculty of Information Technology BUT",
  year="2010",
  month="december",
  pages="0--0",
  publisher="Faculty of Information Technology BUT",
  type="book"
}