In the early 90’s, Bradfield & Stirling developed a sound and complete tableau method for proving that sets of states in infinite-state labelled transition systems satisfy formulas in the modal mu-calculus.

Unfortunately, the soundness proof they presented is not extensible in the following sense. First, it is hard to add new modalities to the mu-calculus, as one would for instance like to do when studying timed modal mu-calculi. Second, when using tableaux to do on-the-fly model checking, one typically resorts to using termination criteria that lead to a sound but not complete approach.

In both cases, essentially one needs to redo the soundness proof presented by Bradfield and Stirling.

In this talk, I present results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices.

I sketch how these results may be used to prove soundness of Bradfield and Stirling’s tableau method.

This is joint work with Rance Cleaveland