Using Accepting Predecessors in Distributed LTL Model-Checking

Warning

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

Authors	MORAVEC Pavel
Year of publication	2004
Type	Article in Proceedings
Conference	MOVEP'04: 6th school on MOdeling and VErifying parallel Processes
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	LTL model checking; distributed algorithm
Description	We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. The influence of the ordering on the algorithm performance is open as future work.
Related projects:	Automated Verification of Parallel and Distributed Systems Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing