Detailed Information on Publication Record
2005
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠABasic information
Original name
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
Name in Czech
Uspořádání vrcholů pro distribuované ověřování LTL vlastností modelu založené na akceptujících předchůdcích
Authors
BRIM, Luboš (203 Czech Republic, guarantor), Ivana ČERNÁ (203 Czech Republic), Pavel MORAVEC (203 Czech Republic) and Jiří ŠIMŠA (203 Czech Republic)
Edition
Lisboa, Portugal, Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), p. 1-12, 2005
Publisher
TU Munchen
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Portugal
Confidentiality degree
není předmětem státního či obchodního tajemství
RIV identification code
RIV/00216224:14330/05:00012461
Organization unit
Faculty of Informatics
Keywords in English
accepting predecessors; LTL model checking
Tags
International impact, Reviewed
Změněno: 22/11/2006 08:32, prof. RNDr. Luboš Brim, CSc.
V originále
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.
In Czech
Č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í.
Links
GA201/03/0509, research and development project |
| ||
GD102/05/H050, research and development project |
| ||
MSM0021622419, plan (intention) |
| ||
1ET408050503, research and development project |
| ||
1M0545, research and development project |
|