Distributed LTL Model-Checking Based on Negative Cycle Detection
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F01%3A00004500" target="_blank" >RIV/00216224:14330/01:00004500 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
čeština
Original language name
Distributed LTL Model-Checking Based on Negative Cycle Detection
Original language description
This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversalof the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.
Czech name
Distributed LTL Model-Checking Based on Negative Cycle Detection
Czech description
—
Classification
Type
D - Article in proceedings
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
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2001
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
FST-TCS 2001
ISBN
3-540-43002-4
ISSN
—
e-ISSN
—
Number of pages
15
Pages from-to
96
Publisher name
Springer
Place of publication
Bangalore, India
Event location
Bangalore, India
Event date
Jan 1, 2001
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—