Tableau-based model checking in the propositional mu-calculus

Summary This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems.Research supported by British Science and Engineering Research Council grant GC/D69464. The results in this paper were obtained while the author was a research associate at the University of Sussex in Brighton, England