Using Assumptions to Distribute CTL Model Checking
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00006432" target="_blank" >RIV/00216224:14330/02:00006432 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Using Assumptions to Distribute CTL Model Checking
Original language description
In this work we discuss the problem of performing distributed CTL model checking by splitting the given state space into several ``partial 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 the truth of formulas and the computers exchangeassumptions about relevant states as they compute more precis
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA201%2F00%2F1023" target="_blank" >GA201/00/1023: Algorithms and tools for practical verification of concurrent systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2002
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
Article name in the collection
1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002)
ISBN
0444512918
ISSN
—
e-ISSN
—
Number of pages
16
Pages from-to
80
Publisher name
Elsevier
Place of publication
Brno, Czech Republic
Event location
August 19, 2002, Brno, Czech republic
Event date
Jan 1, 2002
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—