DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.39

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

Authors: Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.

Cite as

Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas. Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{stoltenow_et_al:LIPIcs.CONCUR.2024.39,
  author =	{Stoltenow, Lara and K\"{o}nig, Barbara and Schneider, Sven and Corradini, Andrea and Lambers, Leen and Orejas, Fernando},
  title =	{{Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.39},
  URN =		{urn:nbn:de:0030-drops-208113},
  doi =		{10.4230/LIPIcs.CONCUR.2024.39},
  annote =	{Keywords: satisfiability, graph conditions, coinductive techniques, category theory}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2020.10

Conditional Bisimilarity for Reactive Systems

Authors: Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We instantiate reactive systems in order to obtain DPO graph rewriting and consider a case study in this setting.

Cite as

Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow. Conditional Bisimilarity for Reactive Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hulsbusch_et_al:LIPIcs.FSCD.2020.10,
  author =	{H\"{u}lsbusch, Mathias and K\"{o}nig, Barbara and K\"{u}pper, Sebastian and Stoltenow, Lara},
  title =	{{Conditional Bisimilarity for Reactive Systems}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.10},
  URN =		{urn:nbn:de:0030-drops-123322},
  doi =		{10.4230/LIPIcs.FSCD.2020.10},
  annote =	{Keywords: conditional bisimilarity, reactive systems, up-to context, graph transformation}
}

Search Results

Documents authored by Stoltenow, Lara

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

Abstract

Cite as

Conditional Bisimilarity for Reactive Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message