Distributed LTL Model-Checking in SPIN

Abstract. In this paper we propose a distributed algorithm for modelchecking 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.

• Type: Conference
• Year: 2001
• Where: SPIN
• Authors: Jiri Barnat, Lubos Brim, Jitka Stríbrná
• Keywords: Depth-first Search Algorithm, Distributed Algorithm, Distributed Version, SPIN 2001, Theoretical Computer Science