Parallel and Symbolic Model Checking for Fixpoint Logic with Chop
Martin Lange, Hans Wolfgang Loidl · Electronic Notes in Theoretical Computer Science · 2005
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 (GpH) and its performance on a cluster of workstations.