4 Search Results for "König, Harald"

Document
DOI: 10.4230/LIPIcs.CSL.2026.24
Well-Founded Coalgebras Meet Kőnig’s Lemma

Authors: Henning Urbat and Thorsten Wißmann

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.
Cite as

Henning Urbat and Thorsten Wißmann. Well-Founded Coalgebras Meet Kőnig’s Lemma. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.CSL.2026.24,
  author =	{Urbat, Henning and Wi{\ss}mann, Thorsten},
  title =	{{Well-Founded Coalgebras Meet K\H{o}nig’s Lemma}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.24},
  URN =		{urn:nbn:de:0030-drops-254485},
  doi =		{10.4230/LIPIcs.CSL.2026.24},
  annote =	{Keywords: K\H{o}nig’s Lemma, Well-Foundedness, Coalgebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.30
A Complete Inference System for Probabilistic Infinite Trace Equivalence

Authors: Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.
Cite as

Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova. A Complete Inference System for Probabilistic Infinite Trace Equivalence. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CSL.2025.30,
  author =	{C\^{i}rstea, Corina and Moss, Lawrence S. and Noquez, Victoria and Schmid, Todd and Silva, Alexandra and Sokolova, Ana},
  title =	{{A Complete Inference System for Probabilistic Infinite Trace Equivalence}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{30:1--30:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.30},
  URN =		{urn:nbn:de:0030-drops-227870},
  doi =		{10.4230/LIPIcs.CSL.2025.30},
  annote =	{Keywords: Coalgebra, infinite trace, semantics, logic, convex sets}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2023.7
Structural Operational Semantics for Heterogeneously Typed Coalgebras

Authors: Harald König, Uwe Wolter, and Tim Kräuter

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

Abstract
Concurrently interacting components of a modular software architecture are heterogeneously structured behavioural models. We consider them as coalgebras based on different endofunctors. We formalize the composition of these coalgebras as specially tailored segments of distributive laws of the bialgebraic approach of Turi and Plotkin. The resulting categorical rules for structural operational semantics involve many-sorted algebraic specifications, which leads to a description of the components together with the composed system as a single holistic behavioural system. We evaluate our approach by showing that observational equivalence is a congruence with respect to the algebraic composition operation.
Cite as

Harald König, Uwe Wolter, and Tim Kräuter. Structural Operational Semantics for Heterogeneously Typed Coalgebras. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{konig_et_al:LIPIcs.CALCO.2023.7,
  author =	{K\"{o}nig, Harald and Wolter, Uwe and Kr\"{a}uter, Tim},
  title =	{{Structural Operational Semantics for Heterogeneously Typed Coalgebras}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{7:1--7: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.7},
  URN =		{urn:nbn:de:0030-drops-188048},
  doi =		{10.4230/LIPIcs.CALCO.2023.7},
  annote =	{Keywords: Coalgebra, Bialgebra, Structural operational semantics, Compositionality}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.16
Being Van Kampen in Presheaf Topoi is a Uniqueness Property

Authors: Harald König and Uwe Wolter

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

Abstract
Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, e.g. the category of directed graphs. Multimodeling requires to construct colimits of diagrams of single models and their instances, while decomposition of instances of the multimodel is given by pullback. Compositionality requires an exact interplay of these operations, i.e., the diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible. In this paper we state a necessary and sufficient yet easily checkable condition for the Van Kampen property to hold for diagrams in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Sobocinski presented at CALCO 2009 the fact that the Van Kampen property reveals a set-based structural uniqueness feature.
Cite as

Harald König and Uwe Wolter. Being Van Kampen in Presheaf Topoi is a Uniqueness Property. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{konig_et_al:LIPIcs.CALCO.2017.16,
  author =	{K\"{o}nig, Harald and Wolter, Uwe},
  title =	{{Being Van Kampen in Presheaf Topoi is a Uniqueness Property}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{16:1--16:15},
  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.16},
  URN =		{urn:nbn:de:0030-drops-80320},
  doi =		{10.4230/LIPIcs.CALCO.2017.16},
  annote =	{Keywords: Van Kampen Cocone, Presheaf Topos, Fibred Semantics, Mapping Path}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2023
  • 1 2017

  • Refine by Author
  • 2 König, Harald
  • 2 Wolter, Uwe
  • 1 Cîrstea, Corina
  • 1 Kräuter, Tim
  • 1 Moss, Lawrence S.
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Semantics and reasoning

  • Refine by Keyword
  • 3 Coalgebra
  • 1 Bialgebra
  • 1 Compositionality
  • 1 Fibred Semantics
  • 1 Kőnig’s Lemma
  • 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