Completeness for coalgebraic fixpoint logic

Research output: Chapter in Book/Report/Conference proceedingPaper in conference proceeding

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 mucalculus. 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.

Details

Authors
  • Sebastian Enqvist
  • Fatemeh Seifan
  • Yde Venema
Organisations
External organisations
  • University of Amsterdam
Research areas and keywords

Subject classification (UKÄ) – MANDATORY

  • Algebra and Logic

Keywords

  • Automata, Coalgebra, Coalgebraic modal logic, Completeness, μ-calculus
Original languageEnglish
Title of host publication25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages7:1
Number of pages7
Volume62
ISBN (Electronic)9783959770224
Publication statusPublished - 2016 Aug 1
Publication categoryResearch
Peer-reviewedYes
Event25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic - Marseille, France
Duration: 2016 Aug 292016 Sep 1

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Volume62
ISSN (Electronic)1868-8969

Conference

Conference25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
CountryFrance
CityMarseille
Period2016/08/292016/09/01