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.
This paper was published in Theoretical Computer Science 96 (1992). pp.157-174. Here is the published version.Previous | Index | Next