Abstract Regular (Tree) Model Checking

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

Result on the web

<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>

Result language

angličtina

Original language name

Abstract Regular (Tree) Model Checking

Original language description

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

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

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

Continuities

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

Publication year

2012

Confidentiality

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

Name of the periodical

International Journal on Software Tools for Technology Transfer

ISSN

1433-2779

e-ISSN

—

Volume of the periodical

14

Issue of the periodical within the volume

2

Country of publishing house

DE - GERMANY

Number of pages

25

Pages from-to

167-191

UT code for WoS article

—

EID of the result in the Scopus database

—