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	2000
Type	Monograph
MU Faculty or unit	Faculty of Informatics
Citation
Description	In this paper we propose a distributed algorithm for model-checking LTL formulas in SPIN. In particular, we explores 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. Some preliminary experimental results are summarised.
Related projects:	Algorithms and tools for practical verification of concurrent systems. Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing