On Reasoning about Infinite-State Systems in the Modal µ-Calculus

Abstract

This paper presents a proof method for proving that infinite-state systems satisfy properties expressed in the modal µ-calculus. The method is sound and complete relative to externally proving inclusions of sets of states. It can be seen as a recast of a tableau method due to Bradfield and Stirling following lines used by Winskel for finite-state systems. Contrary to the tableau method, it avoids the use of constants when unfolding fixed points and it replaces the rather involved global success criterion in the tableau method with local success criteria. A proof tree is now merely a means of keeping track of where possible choices are made -- and can be changed -- and not an essential ingredient in establishing the correctness of a proof: A proof will be correct when all leaves can be directly seen to be valid. Therefore, it seems well-suited for implementation as a tool, by, for instance, integration into existing general-purpose theorem provers.