Uspořádání vrcholů pro distribuované ověřování LTL vlastností modelu založené na akceptujících předchůdcích
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F06%3A00015453" target="_blank" >RIV/00216224:14330/06:00015453 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
Popis výsledku v původním jazyce
The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of acceptingstates (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well.
Název v anglickém jazyce
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
Popis výsledku anglicky
The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of acceptingstates (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2006
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ů
Údaje specifické pro druh výsledku
Název periodika
Electronic Notes in Theoretical Computer Science
ISSN
1571-0661
e-ISSN
—
Svazek periodika
135
Číslo periodika v rámci svazku
2
Stát vydavatele periodika
PT - Portugalská republika
Počet stran výsledku
15
Strana od-do
3-18
Kód UT WoS článku
—
EID výsledku v databázi Scopus
—