Extensible Proof Systems for Infinite-State Systems

TL;DR

This paper develops a lattice-theoretic framework to enhance proof systems for infinite-state systems, enabling sound and complete reasoning for modal mu-calculus and timed modalities.

Contribution

It introduces novel lattice-theoretic results that facilitate the reconstruction and extension of tableau proof methods for infinite-state and timed systems.

Findings

Reconstructed the tableau method for mu-calculus using lattice theory

Extended tableau methods to timed transition systems

Proved soundness and completeness of the extended methods

Abstract

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.