Distributed LTL Model-Checking in SPIN

• Authors: BARNAT Jiří; BRIM Luboš; STŘÍBRNÁ Jitka
• Year of publication: 2000
• Type: Monograph
• MU Faculty or unit: Faculty of Informatics
• 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