Abstract Regular (Tree) Model Checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F12%3APU98200" target="_blank" >RIV/00216305:26230/12:PU98200 - isvavai.cz</a>

Výsledek na webu

<a href="http://www.springerlink.com/content/137uu7118p2054j2/" target="_blank" >http://www.springerlink.com/content/137uu7118p2054j2/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10009-011-0205-y" target="_blank" >10.1007/s10009-011-0205-y</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Abstract Regular (Tree) Model Checking

Popis výsledku v původním jazyce

Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations inregular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verificati

Název v anglickém jazyce

Abstract Regular (Tree) Model Checking

Popis výsledku anglicky

Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, acceleration is needed in the incremental computation of the set of reachable configurations inregular model checking. In this work, we describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate the efficiency of abstract regular (tree) model checking in verificati

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

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

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2012

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ů

Název periodika

International Journal on Software Tools for Technology Transfer

ISSN

1433-2779

e-ISSN

—

Svazek periodika

14

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

25

Strana od-do

167-191

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—