Distributed LTL Model-Checking in SPIN

Warning

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

Authors	BARNAT Jiří BRIM Luboš STŘÍBRNÁ Jitka
Year of publication	2001
Type	Article in Proceedings
Conference	M.B. Dwyer (Ed.): Model Checking Software, 8th International SPIN Workshop
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	model-checking; verification; verification tool
Description	In this paper we propose a distributed algorithm for model-checking LTL. In particular, we explore the possibility of performing nested depth-first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed.
Related projects:	Algorithms and tools for practical verification of concurrent systems. Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing