  This paper revisits soundness and completeness of proof systems for proving
that sets of states in infinite-state labeled transition systems satisfy
formulas in the modal mu-calculus. Our results rely on novel results in lattice
theory, which give constructive characterizations of both greatest and least
fixpoints of monotonic functions over complete lattices. We show how these
results may be used to reconstruct the sound and complete tableau method for
this problem due to Bradfield and Stirling. We also show how the flexibility of
our lattice-theoretic basis simplifies reasoning about tableau-based proof
strategies for alternative classes of systems. In particular, we extend the
modal mu-calculus with timed modalities, and prove that the resulting tableaux
method is sound and complete for timed transition systems.
