How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BRIM Luboš ČERNÁ Ivana MORAVEC Pavel ŠIMŠA Jiří
Year of publication	2006
Type	Article in Periodical
Magazine / Source	Electronic Notes in Theoretical Computer Science
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	accepting predecessors; LTL model checking
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 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.
Related projects:	Automated Verification of Parallel and Distributed Systems Integrated approach to education of PhD students in the area of parallel and distributed systems Techniques for automatic verification and validation of software nad hardware systems Institute for Theoretical Computer Science Highly Parallel and Distributed Computing Systems