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

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

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

Czech name

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

Czech description

V článku je zkoumán problém výpočtu simulací nad stromovými automaty a využití těchto relací pro redukci velikosti stromových automatů. Je popsána metoda výpočtu stromových simulačních relací stojící na převodu daného problému na problém výpočtu klasických simulací nad slovními automaty.<br> Dále navrhujeme metodu kombinace jistých dvou typů simulace (&quot;horní&quot; a &quot;dolní&quot;) tak, aby vznikla relace s ještě lepšími vlastnostmi (vzhledem k redukci stromových automatů). Naše experimentální výsledky potvrzují, že se podařilo přijít s efektivní metodou redukce stromových automatů.<br>

Type

A - Audiovisual production

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

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

ISBN

—

Place of publication

—

Publisher/client name

—

Version

—

Carrier ID

—