Testování univerzality stromových automatů založené na protiřetězcích

Kód výsledku v IS VaVaI

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

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

This report provides the full version of a CIAA'08 paper, in which we propose a new antichain-based algorithms for checking universality and inclusion of nondeterministic tree automata (NTA).&nbsp; We have implemented these algorithms in a prototype tooland 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 entirelyon NTA. We 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.

Název v anglickém jazyce

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

Popis výsledku anglicky

This report provides the full version of a CIAA'08 paper, in which we propose a new antichain-based algorithms for checking universality and inclusion of nondeterministic tree automata (NTA).&nbsp; We have implemented these algorithms in a prototype tooland 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 entirelyon NTA. We 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.

Druh

A - Audiovizuální tvorba

CEP obor

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

OECD FORD obor

—

Projekt

<a href="/cs/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů</a><br>

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

—