Extensible Proof Systems for Infinite-State Systems
From MaRDI portal
Publication:6201709
DOI10.1145/3622786arXiv2207.12953WikidataQ130892429 ScholiaQ130892429MaRDI QIDQ6201709FDOQ6201709
Authors: Rance Cleaveland, Jeroen J. A. Keiren 
Publication date: 21 February 2024
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/2207.12953
Cites Work
- Encyclopaedia of mathematics. Supplement volume III
- Set theory. An introduction to independence proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- CONCUR '90. Theories of concurrency: unification and extension. Amsterdam, The Netherlands, August 1990. Proceedings
- Proceedings of the eleventh annual ACM symposium on Principles of distributed computing - PODC '92
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)
