Distributed LTL Model-Checking Based on Negative Cycle Detection

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

čeština

Název v původním jazyce

Distributed LTL Model-Checking Based on Negative Cycle Detection

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Distributed LTL Model-Checking Based on Negative Cycle Detection

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2001

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

FST-TCS 2001

ISBN

3-540-43002-4

ISSN

—

e-ISSN

—

Počet stran výsledku

15

Strana od-do

96

Název nakladatele

Springer

Místo vydání

Bangalore, India

Místo konání akce

Bangalore, India

Datum konání akce

1. 1. 2001

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

WRD - Celosvětová akce

Kód UT WoS článku

—