Distributed LTL Model-Checking in SPIN

• 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
• 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