Tableau-based model checking in the propositional mu-calculus (Q1122572)

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.