BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. Electronic Notes in Theoretical Computer Science. Nizozemsko: Elsevier, 2006, roč. 135, č. 2, s. 3-18, 15 s. ISSN 1571-0661. |
Další formáty:
BibTeX
LaTeX
RIS
@article{702503, author = {Brim, Luboš and Černá, Ivana and Moravec, Pavel and Šimša, Jiří}, article_location = {Nizozemsko}, article_number = {2}, keywords = {accepting predecessors; LTL model checking}, language = {eng}, issn = {1571-0661}, journal = {Electronic Notes in Theoretical Computer Science}, title = {How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors}, volume = {135}, year = {2006} }
TY - JOUR ID - 702503 AU - Brim, Luboš - Černá, Ivana - Moravec, Pavel - Šimša, Jiří PY - 2006 TI - How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors JF - Electronic Notes in Theoretical Computer Science VL - 135 IS - 2 SP - 3-18 EP - 3-18 PB - Elsevier SN - 15710661 KW - accepting predecessors KW - LTL model checking N2 - 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 accepting states (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. ER -
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. \textit{Electronic Notes in Theoretical Computer Science}. Nizozemsko: Elsevier, 2006, roč.~135, č.~2, s.~3-18, 15 s. ISSN~1571-0661.
|