Extensible Proof Systems for Infinite-State Systems

DOI10.1145/3622786MaRDI QIDQ6201709WikidataFDO

Authors Rance Cleaveland, Jeroen J. A. Keiren

Publication date 21 February 2024

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2207.12953

zbMATH Keywords

model checkingmu-calculustableauxinfinite-state systemstimed systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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.

Cites work

• scientific article; zbMATH DE number 3652325 (Why is no real title available?)
• scientific article; zbMATH DE number 1198604 (Why is no real title available?)
• CONCUR '90. Theories of concurrency: unification and extension. Amsterdam, The Netherlands, August 1990. Proceedings
• Encyclopaedia of mathematics. Supplement volume III
• Proceedings of the eleventh annual ACM symposium on Principles of distributed computing - PODC '92
• Set theory. An introduction to independence proofs

This page was built for publication: Extensible Proof Systems for Infinite-State Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6201709)