3 Search Results for "Poiger, Wolfgang"

Document
DOI: 10.4230/LIPIcs.CALCO.2025.9
Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Authors: Helle Hvid Hansen and Wolfgang Poiger

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra 𝐀 of truth-degrees. More precisely, we work with coalgebraic modal logic via 𝐀-valued predicate liftings where 𝐀 is an FLew-algebra, and interpret actions (abstracting programs and games) as 𝖥-coalgebras where the functor 𝖥 represents some type of 𝐀-weighted system. We also allow combinations of crisp propositions with 𝐀-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 𝟐-valued iteration-free PDL with 𝐀-valued accessibility relations when 𝐀 is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.
Cite as

Helle Hvid Hansen and Wolfgang Poiger. Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hansen_et_al:LIPIcs.CALCO.2025.9,
  author =	{Hansen, Helle Hvid and Poiger, Wolfgang},
  title =	{{Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{9:1--9:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.9},
  URN =		{urn:nbn:de:0030-drops-235681},
  doi =		{10.4230/LIPIcs.CALCO.2025.9},
  annote =	{Keywords: dynamic logic, many-valued coalgebraic logic, safety, strong completeness}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CALCO.2025.2
Logic Enriched over a Quantale (Invited Talk)

Authors: Alexander Kurz

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Many-valued logics have a long history in mathematical logic as well as in applications to the semantics of programming languages and to engineering more generally. Typically these logics are rich with features motivated by the particular applications they stem from. In his 1973 article "Metric Spaces, Generalized Logic, and Closed Categories", Lawvere argued that any quantale Ω gives rise to a generalized Ω-valued logic that has as its models the categories enriched over the quantale. This suggests developing a uniform framework for many-valued logics parameterized in a quantale. In this talk we will review some previous and ongoing work in that direction. In particular, we will address (not necessarily answer) the following questions. - If we take as our starting point, generalizing from 2-valued lattice logic, a logical language that comprises not only meets and joins (limits and colimits) but also tensor and power (weighted limits and colimits), what laws do these operations satisfy? - This question can be investigated for different types of semantics, generalizing the set-theoretic and the polarity-based semantics known from the 2-valued setting. - Which additional properties obtain if the quantale is integral or commutative or finite or distributive, etc? - On the other hand, quantale logics can also be investigated from a purely proof theoretic point of view, leading us to consider sequent calculi with turnstiles ⊢_ω labelled by elements ω ∈ Ω. - As Galatos and Jipsen showed, there are 1662 "Residuated Lattices of Size up to 6". Each of them generates a different and potentially interesting logic. - The adjunction Ω^-⊣ Ω^-:Ω-cat^op → Ω-cat exists for any quantale Ω. What is the logic enshrined in the monad of that adjunction? How far can one extend this to a theory of Stone duality for quantale logics parametric in the quantale? - The Dedekind-MacNeille completion generalizes to quantale categories. Similarly, the theory of canonical extensions originating with Jonsson and Tarski (and important for completeness proofs of modal logics) can be extended to quantale logics. - Since the discrete functor Set → Ω-cat is dense in the sense of Kelly, set-functors (equipped with an Ω-cat structure or not) can be extended to quantale categories via enriched left Kan extensions. This gives rise to a uniform variety of type constructors (endofunctors) on quantale categories parameterised by the quantale. - Each endofunctor on Ω-cat gives rise to a category of coalgebras with their own notion of behavioural equivalence. How many of the existing notions of many-valued (probabilistic, metric, fuzzy, etc) bisimulation can be accounted for in this uniform framework? - Morphism between quantales gives rise to change-of-base principles between categories of (co)algebras. Which transfer principles can be obtained from a systematic investigation of change of base for quantale categories? - Exploiting the duality of coalgebras (as models of computation) and algebras (as modal logics), which general logical theory of computation arises from putting the items in this list together?
Cite as

Alexander Kurz. Logic Enriched over a Quantale (Invited Talk). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kurz:LIPIcs.CALCO.2025.2,
  author =	{Kurz, Alexander},
  title =	{{Logic Enriched over a Quantale}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.2},
  URN =		{urn:nbn:de:0030-drops-235609},
  doi =		{10.4230/LIPIcs.CALCO.2025.2},
  annote =	{Keywords: Modal Logic, Coalgebra, Enriched Category Theory}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2023.17
Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties

Authors: Alexander Kurz and Wolfgang Poiger

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
We study many-valued coalgebraic logics with primal algebras of truth-degrees. We describe a way to lift algebraic semantics of classical coalgebraic logics, given by an endofunctor on the variety of Boolean algebras, to this many-valued setting, and we show that many important properties of the original logic are inherited by its lifting. Then, we deal with the problem of obtaining a concrete axiomatic presentation of the variety of algebras for this lifted logic, given that we know one for the original one. We solve this problem for a class of presentations which behaves well with respect to a lattice structure on the algebra of truth-degrees.
Cite as

Alexander Kurz and Wolfgang Poiger. Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kurz_et_al:LIPIcs.CALCO.2023.17,
  author =	{Kurz, Alexander and Poiger, Wolfgang},
  title =	{{Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.17},
  URN =		{urn:nbn:de:0030-drops-188147},
  doi =		{10.4230/LIPIcs.CALCO.2023.17},
  annote =	{Keywords: coalgebraic modal logic, many-valued logic, primal algebras, algebraic semantics, presenting functors}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2023

  • Refine by Author
  • 2 Kurz, Alexander
  • 2 Poiger, Wolfgang
  • 1 Hansen, Helle Hvid

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Theory of computation
  • 1 Theory of computation → Algebraic semantics
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Program reasoning

  • Refine by Keyword
  • 1 Coalgebra
  • 1 Enriched Category Theory
  • 1 Modal Logic
  • 1 algebraic semantics
  • 1 coalgebraic modal logic
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact