Document Open Access Logo

Completeness for Coalgebraic Fixpoint Logic

Authors Sebastian Enqvist, Fatemeh Seifan, Yde Venema

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.7.pdf
  • Filesize: 0.61 MB
  • 19 pages

Document Identifiers

Author Details

Sebastian Enqvist
Fatemeh Seifan
Yde Venema

Cite As Get BibTex

Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. Completeness for Coalgebraic Fixpoint Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.7

Abstract

We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss' coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss'modality, extended with Kozen's axiom and rule for the fixpoint operators.

Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result.

The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz' proof.

Subject Classification

Keywords
  • mu-calculus
  • coalgebra
  • coalgebraic modal logic
  • automata
  • completeness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J. Richard Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(1-6):66-92, 1960. Google Scholar
  2. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: Interpolation, lyndon and ł oś-tarski. Journal of Symbolic Logic, 65(1):310-332, 2000. Google Scholar
  3. Gäelle Fontaine, Raul Leal, and Yde Venema. Automata for coalgebras: An approach using predicate liftings. In Automata, Languages and Programming: 37th International Colloquium ICALP'10, pages 381-392, 2010. Google Scholar
  4. David Janin and Igor Walukiewicz. Automata for the modal μ-calculus and related results. In 20th Symposium on Mathematical Foundations of Computer Science MFCS'95, volume 969, pages 552-562, 1995. Google Scholar
  5. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In 7th International Conference on Concurrency Theory CONCUR'96, pages 263-277, 1996. Google Scholar
  6. Christian Kissig and Yde Venema. Complementation of coalgebra automata. In 3rd Conference on Algebra and Coalgebra in Computer Science CALCO'09, pages 81-96, 2009. Google Scholar
  7. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Google Scholar
  8. Clemens Kupke, Alexander Kurz, and Yde Venema. Completeness of the finitary Moss logic. In 9th Conference on Advances in Modal Logic AiML'08, pages 193-217, 2008. Google Scholar
  9. Clemens Kupke, Alexander Kurz, and Yde Venema. Completeness for the coalgebraic cover modality. Logical Methods in Computer Science, 8:1-76, 2012. Google Scholar
  10. Clemens Kupke and Yde Venema. Coalgebraic automata theory: Basic results. Logical Methods in Computer Science, 4(4), 2008. Google Scholar
  11. Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform interpolation for coalgebraic fixpoint logic. In 6th Conference on Algebra and Coalgebra in Computer Science CALCO'15, pages 238-252, 2015. Google Scholar
  12. Larry Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96:277-317, 1999. (Erratum published Ann.P.Appl.Log. 99:241-259, 1999). Google Scholar
  13. David E. Muller and Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141(1-2):69-107, 1995. Google Scholar
  14. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  15. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. Google Scholar
  16. Luigi Santocanale. Free μ-lattices. Journal of Pure and Applied Algebra, 168(2-3):227-264, 2002. Category Theory 1999: selected papers, conference held in Coimbra in honour of the 90th birthday of Saunders Mac Lane. Google Scholar
  17. Yde Venema. Automata and fixed point logic: a coalgebraic perspective. Information and Computation, 204:637-678, 2006. Google Scholar
  18. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157:142-182, 2000. Google Scholar
  19. Thomas Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bulletin of the Belgian Mathematical Society - Simon Stevin, 8(2):359-391, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact