Abstract Regular Tree Model Checking
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F06%3APU66852" target="_blank" >RIV/00216305:26230/06:PU66852 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Abstract Regular Tree Model Checking
Original language description
Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finiteword or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachableconfigurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which
Czech name
Abstraktní regulární model checking nad stromy
Czech description
Článek zobecňuje dříve zavedenou metodu abstraktního regulárního model checkingu nad systémy s lineární (linearizovatelnou) strukturou na systémy se stromovu strukturou stavů. K representaci nekonečných množin stavů takových systémů jsou použity konečnéstromové automaty.
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2006
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
ISSN
1571-0661
e-ISSN
—
Volume of the periodical
149
Issue of the periodical within the volume
1
Country of publishing house
US - UNITED STATES
Number of pages
12
Pages from-to
37-48
UT code for WoS article
—
EID of the result in the Scopus database
—