Technical Report No. 176 - Abstract

Alberto Lluch Lafuente
Simplified Distributed LTL Model Checking by Localizing Cycles

Distributed Model Checking avoids the state explosion problem by using the computational resources of parallel environments LTL model checking mainly entails detecting accepting cycles in a state transition graph. The nested depth-first search algorithm used for this purpose is difficult to parallelize since it is based on the depth-first search traversal order which is inherently sequential. Proposed solutions make use of data structures and synchronization mechanisms in order to preserve the depth-first order. We propose a simple distributed algorithm that assumes cycles to be localized by the partition function. Cycles can then be checked without requiring particular synchronization mechanisms. Methods for constructing such kind of partition functions are also proposed. The algorithm has a limited application since it highly depends on the monotonic behavior of the model to be checked.