DROPS

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}
}

Search Results

Documents authored by Wolter, Uwe

Structural Operational Semantics for Heterogeneously Typed Coalgebras

Abstract

Cite as

Being Van Kampen in Presheaf Topoi is a Uniqueness Property

Abstract

Cite as

Thanks for your feedback!

Could not send message