Parallel and Symbolic Model Checking for Fixpoint Logic with Chop

Martin Lange, Hans Wolfgang Loidl


We consider the model checking problem for FLC, a modal fixpoint logic capable of defining non-regular properties. This paper presents a refinement of a symbolic model checker and discusses how to parallelise this algorithm. It reports on a prototype implementation of the algorithm in Glasgow Parallel Haskell and its performance on a cluster of workstations.