2005
Assumption-based distribution of CTL model checking
BRIM, Luboš, Jitka ŽIDKOVÁ a Karen YORAVZákladní údaje
Originální název
Assumption-based distribution of CTL model checking
Název česky
Distribuované ověřování modelu CTL založené na předpokladech
Autoři
BRIM, Luboš (203 Česká republika, garant), Jitka ŽIDKOVÁ (203 Česká republika) a Karen YORAV (376 Izrael)
Vydání
International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 2005, 1433-2779
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Německo
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/05:00012429
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
model-checking
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 08:32, prof. RNDr. Luboš Brim, CSc.
V originále
In this paper we discuss the problem of performing distributed CTL model checking by splitting the given state space into several ldquopartial state spaces. The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model-checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about truth values of formulas and the computers exchange assumptions about relevant states to compute more precise information.
Česky
Je navržena distribuce ověřování modelu pro logiku CTL, která modeluje částečné stavové prostory jako Kripkeho struktury s hraničními stavy. Algoritmus je založen na využití předpokladů o pravdivosti formulí v hraničních stavech, počítače postupně upřesňují předpoklady výměnou relevantních informací.
Návaznosti
| GA201/03/0509, projekt VaV |
| ||
| MSM0021622419, záměr |
|