Search Results

Documents authored by Beohar, Harsh

Document
DOI: 10.4230/LIPIcs.STACS.2024.10
Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach

Authors: Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on an earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).
Cite as

Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beohar_et_al:LIPIcs.STACS.2024.10,
  author =	{Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla and Forster, Jonas and Schr\"{o}der, Lutz and Wild, Paul},
  title =	{{Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.10},
  URN =		{urn:nbn:de:0030-drops-197203},
  doi =		{10.4230/LIPIcs.STACS.2024.10},
  annote =	{Keywords: modal logics, coalgebras, behavioural equivalences, behavioural metrics, linear-time semantics, Eilenberg-Moore categories}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2023.6
Forward and Backward Steps in a Fibration

Authors: Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot

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

Abstract
Distributive laws of various kinds occur widely in the theory of coalgebra, for instance to model automata constructions and trace semantics, and to interpret coalgebraic modal logic. We study steps, which are a general type of distributive law, that allow one to map coalgebras along an adjunction. In this paper, we address the question of what such mappings do to well known notions of equivalence, e.g., bisimilarity, behavioural equivalence, and logical equivalence. We do this using the characterisation of such notions of equivalence as (co)inductive predicates in a fibration. Our main contribution is the identification of conditions on the interaction between the steps and liftings, which guarantees preservation of fixed points by the mapping of coalgebras along the adjunction. We apply these conditions in the context of lax liftings proposed by Bonchi, Silva, Sokolova (2021), and generalise their result on preservation of bisimilarity in the construction of a belief state transformer. Further, we relate our results to properties of coalgebraic modal logics including expressivity and completeness.
Cite as

Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot. Forward and Backward Steps in a Fibration. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{turkenburg_et_al:LIPIcs.CALCO.2023.6,
  author =	{Turkenburg, Ruben and Beohar, Harsh and Kupke, Clemens and Rot, Jurriaan},
  title =	{{Forward and Backward Steps in a Fibration}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{6:1--6:18},
  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.6},
  URN =		{urn:nbn:de:0030-drops-188032},
  doi =		{10.4230/LIPIcs.CALCO.2023.6},
  annote =	{Keywords: Coalgebra, Fibration, Bisimilarity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.12
Hennessy-Milner Theorems via Galois Connections

Authors: Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We introduce a general and compositional, yet simple, framework that allows to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular, this framework allows to derive a new fixpoint characterization of directed trace metrics.
Cite as

Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner Theorems via Galois Connections. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{beohar_et_al:LIPIcs.CSL.2023.12,
  author =	{Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla},
  title =	{{Hennessy-Milner Theorems via Galois Connections}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.12},
  URN =		{urn:nbn:de:0030-drops-174735},
  doi =		{10.4230/LIPIcs.CSL.2023.12},
  annote =	{Keywords: behavioural equivalences and metrics, modal logics, Galois connections}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.6
On Path-Based Coalgebras and Weak Notions of Bisimulation

Authors: Harsh Beohar and Sebastian Küpper

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

Abstract
It is well known that the theory of coalgebras provides an abstract definition of behavioural equivalence that coincides with strong bisimulation across a wide variety of state-based systems. Unfortunately, the theory in the presence of so-called silent actions is not yet fully developed. In this paper, we give a coalgebraic characterisation of branching (delay) bisimulation in the context of labelled transition systems (fully probabilistic systems). It is shown that recording executions (up to a notion of stuttering), rather than the set of successor states, from a state is sufficient to characterise the respected bisimulation relations in both cases.
Cite as

Harsh Beohar and Sebastian Küpper. On Path-Based Coalgebras and Weak Notions of Bisimulation. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{beohar_et_al:LIPIcs.CALCO.2017.6,
  author =	{Beohar, Harsh and K\"{u}pper, Sebastian},
  title =	{{On Path-Based Coalgebras and Weak Notions of Bisimulation}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{6:1--6:17},
  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.6},
  URN =		{urn:nbn:de:0030-drops-80362},
  doi =		{10.4230/LIPIcs.CALCO.2017.6},
  annote =	{Keywords: Paths, Executions, Branching bisimulation, Coalgebras}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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