How to distribute LTL model-checking using decomposition of negative claim automaton
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00007074" target="_blank" >RIV/00216224:14330/02:00007074 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
How to distribute LTL model-checking using decomposition of negative claim automaton
Original language description
We propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm.
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
SOFSEM 2002 Student Research Forum Proceedings
ISBN
—
ISSN
—
e-ISSN
—
Number of pages
6
Pages from-to
9
Publisher name
Slovak University of Technology
Place of publication
Milovy,Czech Republic
Event location
Milovy Czech Republic, November 27, 2002
Event date
Jan 1, 2002
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
—