4 Search Results for "Beohar, Harsh"


Document
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
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
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}
}
Document
Invited Paper
Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap (Invited Paper)

Authors: Narges Khakpour and Mohammad Reza Mousavi

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
We review and compare three notions of conformance testing for cyber-physical systems. We begin with a review of their underlying semantic models and present conformance-preserving translations between them. We identify the differences in the underlying semantic models and the various design decisions that lead to these substantially different notions of conformance testing. Learning from this exercise, we reflect upon the challenges in designing an "ideal" notion of conformance for cyber-physical systems and sketch a roadmap of future research in this domain.

Cite as

Narges Khakpour and Mohammad Reza Mousavi. Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 18-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{khakpour_et_al:LIPIcs.CONCUR.2015.18,
  author =	{Khakpour, Narges and Mousavi, Mohammad Reza},
  title =	{{Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{18--40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.18},
  URN =		{urn:nbn:de:0030-drops-53975},
  doi =		{10.4230/LIPIcs.CONCUR.2015.18},
  annote =	{Keywords: Cyber-physical systems, hybrid systems, conformance testing, model-based testing, behavioral pre-orders, hybrid input-output conformance testing, (tau}
}
  • Refine by Author
  • 3 Beohar, Harsh
  • 1 Gurke, Sebastian
  • 1 Khakpour, Narges
  • 1 Kupke, Clemens
  • 1 König, Barbara
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 1 (tau
  • 1 Bisimilarity
  • 1 Branching bisimulation
  • 1 Coalgebra
  • 1 Coalgebras
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2015
  • 1 2017

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