Advanced

Completeness for coalgebraic fixpoint logic

Enqvist, Sebastian LU ; Seifan, Fatemeh and Venema, Yde (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.1-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 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... (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 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.

(Less)
Please use this url to cite or link to this publication:
author
organization
publishing date
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- Leibniz-Zentrum 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
2016-08-29 - 2016-09-01
external identifiers
  • scopus:85012898718
ISSN
1868-8969
ISBN
9783959770224
DOI
10.4230/LIPIcs.CSL.2016.7
language
English
LU publication?
yes
id
e478b4ac-64e7-4936-9c76-c855182f7adb
date added to LUP
2017-03-02 08:32:54
date last changed
2020-04-01 06:01:14
@inproceedings{e478b4ac-64e7-4936-9c76-c855182f7adb,
  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 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.</p>},
  author       = {Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde},
  booktitle    = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  isbn         = {9783959770224},
  issn         = {1868-8969},
  language     = {eng},
  month        = {08},
  pages        = {1--7},
  publisher    = {Schloss Dagstuhl- Leibniz-Zentrum 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},
}