The paper Extensible Proof Systems for Infinite-State Systems by Rance Cleaveland and Jeroen Keiren has appeared in ACM Transactions on Computational Logic.

The 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 in order to develop proof techniques that permit the seamless inclusion of new features in this logic. The approach relies on results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices.

The paper is available open access from https://doi.org/10.1145/3622786