Completeness for coalgebraic fixpoint logic
(2016) 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic In Leibniz International Proceedings in Informatics (LIPIcs) 62. p.17 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... (More)
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.
(Less)
 author
 Enqvist, Sebastian ^{LU} ; Seifan, Fatemeh and Venema, Yde
 organization
 publishing date
 20160801
 type
 Chapter in Book/Report/Conference proceeding
 publication status
 published
 subject
 keywords
 Automata, Coalgebra, Coalgebraic modal logic, Completeness, μcalculus
 host publication
 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
 series title
 Leibniz International Proceedings in Informatics (LIPIcs)
 volume
 62
 pages
 7 pages
 publisher
 Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing
 conference name
 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
 conference location
 Marseille, France
 conference dates
 20160829  20160901
 external identifiers

 scopus:85012898718
 ISSN
 18688969
 ISBN
 9783959770224
 DOI
 10.4230/LIPIcs.CSL.2016.7
 language
 English
 LU publication?
 yes
 id
 e478b4ac64e749369c76c855182f7adb
 date added to LUP
 20170302 08:32:54
 date last changed
 20200401 06:01:14
@inproceedings{e478b4ac64e749369c76c855182f7adb, abstract = {<p>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.</p>}, author = {Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, isbn = {9783959770224}, issn = {18688969}, language = {eng}, month = {08}, pages = {17}, publisher = {Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Completeness for coalgebraic fixpoint logic}, url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.7}, doi = {10.4230/LIPIcs.CSL.2016.7}, volume = {62}, year = {2016}, }