Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata

Result code in IS VaVaI

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

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata

Original language description

We propose new antichain-based algorithms for<br>checking universality and inclusion of nondeterministic tree automata (NTA). <br>We have<br>implemented these algorithms in a prototype tool and our experiments<br>show that they provide a significant improvement over the traditional<br>determinisation-based approaches. We use our<br>antichain-based inclusion checking algorithm to build an abstract regular tree<br>model checking framework based entirely on NTA. We<br>show the significantly improved efficiency of this&nbsp; framework through a series of experiments with verifying various programs over dynamic linked tree-shaped data structures.

Czech name

—

Czech description

—

Type

D - Article in proceedings

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ů

Article name in the collection

Implementation and Application of Automata

ISBN

978-3-540-70843-8

ISSN

—

e-ISSN

—

Number of pages

11

Pages from-to

—

Publisher name

Springer Verlag

Place of publication

Berlin

Event location

San Francisco, California

Event date

Jul 21, 2008

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—