How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
The result's identifiers
Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
Original language description
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.
Czech name
Uspořádání vrcholů pro distribuované ověřování LTL vlastností modelu založené na akceptujících předchůdcích
Czech description
Článek zkoumá problém optimálního uspořádání dříve prezentovaného algoritmu pro distribuované ověřování LTL vlastností modelu a prezentuje několik heuristik pro nalezení optimálního uspořádání v distribuovaném prostředí.
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2006
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Electronic Notes in Theoretical Computer Science
ISSN
1571-0661
e-ISSN
—
Volume of the periodical
135
Issue of the periodical within the volume
2
Country of publishing house
PT - PORTUGAL
Number of pages
15
Pages from-to
3-18
UT code for WoS article
—
EID of the result in the Scopus database
—