Distributed breadth-first search LTL model checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F06%3A00015452" target="_blank" >RIV/00216224:14330/06:00015452 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Distributed breadth-first search LTL model checking
Original language description
We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for networks of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so-called back-level edges. In particular, a parallel level synchronized breadth-first search of the graph is performed to discover all back-level edges, and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several improvements of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed.
Czech name
Distribuované ověřování modelu LTL s využitím prohledávání grafu do šířky
Czech description
Je zde navrhnut a experimentalně vyhodnocen algoritmus pro detekci akceptujicích cyklů v grafu, založený na tzv. back-level hranách. Algoritmus je dále rozšířen o několik nezbytných módů, které jsou nezbytné pro vytvoření skutečného verifikačního nástroje pro LTL ověřování modelů. Tento nástroj byl implementován a experimentálně vyhodnocen na několika směrodatných vstupech.

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2006
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)