Detail publikace

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

Originální název

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

Anglický název

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

Jazyk

en

Originální abstrakt

The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking.

Anglický abstrakt

The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking.

BibTex


@article{BUT76407,
  author="Lukáš {Holík} and Ondřej {Lengál} and Jiří {Šimáček} and Tomáš {Vojnar}",
  title="Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata",
  annote="The paper considers several issues related to efficient use of tree automata in
formal verification. First, a new efficient algorithm for inclusion checking on
non-deterministic tree automata is proposed. The algorithm traverses the
automaton downward, utilizing antichains and simulations to optimize its run.
Results of a set of experiments are provided, showing that such an approach often
very significantly outperforms the so far common upward inclusion checking. Next,
a new semi-symbolic representation of non-deterministic tree automata, suitable
for automata with huge alphabets, is proposed together with algorithms for upward
as well as downward inclusion checking over this representation of tree automata.
Results of a set of experiments comparing the performance of these algorithms are
provided, again showing that the newly proposed downward inclusion is very often
better than upward inclusion checking.",
  address="NEUVEDEN",
  chapter="76407",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="6996",
  volume="2011",
  year="2011",
  month="october",
  pages="243--258",
  publisher="NEUVEDEN",
  type="journal article - other"
}