Výpočet simulací nad stromovými automaty: Efektivní techniky redukce stromových automatů

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU78048" target="_blank" >RIV/00216305:26230/08:PU78048 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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 ef&amp;#64257;cient 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 ef&amp;#64257;cient size reduction of nondeterministic tree automata. This is of a very high interest, for instance, for symbolic veri&amp;#64257;cation methods suchas regular model checking, which use tree automata to represent in&amp;#64257;nite sets of reachable con&amp;#64257;gurations. We provide experimental results showing the ef&amp;#64257;ciency of our algorithms on examples of tree automat

Název v anglickém jazyce

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

Popis výsledku anglicky

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 ef&amp;#64257;cient 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 ef&amp;#64257;cient size reduction of nondeterministic tree automata. This is of a very high interest, for instance, for symbolic veri&amp;#64257;cation methods suchas regular model checking, which use tree automata to represent in&amp;#64257;nite sets of reachable con&amp;#64257;gurations. We provide experimental results showing the ef&amp;#64257;ciency of our algorithms on examples of tree automat

Druh

A - Audiovizuální tvorba

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2008

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

—

Místo vydání

—

Název nakladatele resp. objednatele

—

Verze

—

Identifikační číslo nosiče

—