2 Search Results for "Enqvist, Sebastian"

Document

DOI: 10.4230/LIPIcs.CALCO.2017.11

Disjunctive Bases: Normal Forms for Modal Logics

Authors: Sebastian Enqvist and Yde Venema

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract

We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "one-step" level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full fixpoint logic, its fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive bases, and provide a partial solution.

Cite as

Sebastian Enqvist and Yde Venema. Disjunctive Bases: Normal Forms for Modal Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{enqvist_et_al:LIPIcs.CALCO.2017.11,
  author =	{Enqvist, Sebastian and Venema, Yde},
  title =	{{Disjunctive Bases: Normal Forms for Modal Logics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.11},
  URN =		{urn:nbn:de:0030-drops-80357},
  doi =		{10.4230/LIPIcs.CALCO.2017.11},
  annote =	{Keywords: Modal logic, fixpoint logic, automata, coalgebra, graded modal logic, Lyndon theorem, uniform interpolation}
}

Document

DOI: 10.4230/LIPIcs.CSL.2016.7

Completeness for Coalgebraic Fixpoint Logic

Authors: Sebastian Enqvist, Fatemeh Seifan, and Yde Venema

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{enqvist_et_al:LIPIcs.CSL.2016.7,
  author =	{Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde},
  title =	{{Completeness for Coalgebraic Fixpoint Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.7},
  URN =		{urn:nbn:de:0030-drops-65470},
  doi =		{10.4230/LIPIcs.CSL.2016.7},
  annote =	{Keywords: mu-calculus, coalgebra, coalgebraic modal logic, automata, completeness}
}

Refine by Author
2 Enqvist, Sebastian
2 Venema, Yde
1 Seifan, Fatemeh

Refine by Classification

Refine by Keyword
2 automata
2 coalgebra
1 Lyndon theorem
1 Modal logic
1 coalgebraic modal logic
Show More...

Refine by Type
2 document

Refine by Publication Year
1 2016
1 2017

2 Search Results for "Enqvist, Sebastian"

Disjunctive Bases: Normal Forms for Modal Logics

Abstract

Cite as

Completeness for Coalgebraic Fixpoint Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message