Distributed Explicit Bounded LTL Model Checking
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F03%3A00009020" target="_blank" >RIV/00216224:14330/03:00009020 - isvavai.cz</a>
Alternative codes found
RIV/00216224:14330/03:00008587
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Distributed Explicit Bounded LTL Model Checking
Original language description
Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method - model checking - is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automated Verification of Parallel and Distributed Systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2003
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
Second International Workshop on Parallel and Distributed Model Checking
ISBN
—
ISSN
—
e-ISSN
—
Number of pages
18
Pages from-to
30
Publisher name
Elsevier
Place of publication
Neuveden
Event location
Boulder, Colorado, USA
Event date
Jan 1, 2003
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—