Enqvist, Sebastian ;
Seifan, Fatemeh ;
Venema, Yde
Completeness for Coalgebraic Fixpoint Logic
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 wellknown modal mucalculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mucalculus 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 automatatheoretic 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 KozenWalukiewicz completeness theorem for the modal mucalculus, and our automatatheoretic methods simplify parts of Walukiewicz' proof.
BibTeX  Entry
@InProceedings{enqvist_et_al:LIPIcs:2016:6547,
author = {Sebastian Enqvist and Fatemeh Seifan and Yde Venema},
title = {{Completeness for Coalgebraic Fixpoint Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {7:17:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770224},
ISSN = {18688969},
year = {2016},
volume = {62},
editor = {JeanMarc Talbot and Laurent Regnier},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6547},
URN = {urn:nbn:de:0030drops65470},
doi = {10.4230/LIPIcs.CSL.2016.7},
annote = {Keywords: mucalculus, coalgebra, coalgebraic modal logic, automata, completeness}
}
2016
Keywords: 

mucalculus, coalgebra, coalgebraic modal logic, automata, completeness 
Seminar: 

25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Issue date: 

2016 
Date of publication: 

2016 