Akceptující předchůdci v distrubuovaném LTL ověřování modelů

Kód výsledku v IS VaVaI

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

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.

Popis výsledku v původním jazyce

We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and thesubsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.

Název v anglickém jazyce

Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.

Popis výsledku anglicky

We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and thesubsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising 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

Formal Methods in Computer-Aided Design (FMCAD)

ISBN

3-540-23738-0

ISSN

—

e-ISSN

—

Počet stran výsledku

24

Strana od-do

352-366

Název nakladatele

Springer-Verlag, LNCS 3312

Místo vydání

Neuveden

Místo konání akce

Austin, USA

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

—