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

Result code in IS VaVaI

RIV/00216305:26230/08:PU76752 - isvavai.cz

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
checking universality and inclusion of nondeterministic tree automata (NTA).
We have
implemented these algorithms in a prototype tool and our experiments
show that they provide a significant improvement over the traditional
determinisation-based approaches. We use our
antichain-based inclusion checking algorithm to build an abstract regular tree
model checking framework based entirely on NTA. We
show the significantly improved efficiency of this  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

—