Local Model Checking for Infinite State Spaces

Julian Bradfield and Colin Stirling

Abstract: We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.

LFCS report ECS-LFCS-90-115

This paper was published in Theoretical Computer Science 96 (1992). pp.157-174. Here is the published version.

Previous | Index | Next