Od distribuovane detekce cyklu k paralelnimu LTL overovani modelu

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010725" target="_blank" >RIV/00216224:14330/04:00010725 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

From Distributed Memory Cycle Detection to Parallel LTL Model Checking

Popis výsledku v původním jazyce

We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn thealgorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results.

Název v anglickém jazyce

From Distributed Memory Cycle Detection to Parallel LTL Model Checking

Popis výsledku anglicky

We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn thealgorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automatizovaná verifikace paralelních a distribuovaných systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2004

Kód důvěrnosti údajů

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

Název statě ve sborníku

Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)

ISBN

3-902457-03-1

ISSN

—

e-ISSN

—

Počet stran výsledku

18

Strana od-do

17-34

Název nakladatele

Institute for Systems Engineering & Automation, Kepler university Linz

Místo vydání

Linz, Austria

Místo konání akce

Linz, Austria

Datum konání akce

1. 1. 2004

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—