Search Results

Documents authored by König, Barbara

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.20
Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques

Authors: Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild

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

Abstract
Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the category theoretic generalization of the Kantorovich lifting from transportation theory to the case of lifting functors to quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition, we describe how to lift distributive laws in the case where one of the two functors is polynomial (with finite coproducts). These results are essential ingredients for adapting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We illustrate the results of our paper in two case studies.
Cite as

Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild. Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dangelo_et_al:LIPIcs.CONCUR.2024.20,
  author =	{D'Angelo, Keri and Gurke, Sebastian and Kirss, Johanna Maria and K\"{o}nig, Barbara and Najafi, Matina and R\'{o}\.{z}owski, Wojciech and Wild, Paul},
  title =	{{Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{20:1--20:19},
  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.20},
  URN =		{urn:nbn:de:0030-drops-207921},
  doi =		{10.4230/LIPIcs.CONCUR.2024.20},
  annote =	{Keywords: behavioural metrics, coalgebra, Galois connections, quantales, Kantorovich lifting, up-to techniques}
}
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.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
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2024.4
Approximating Fixpoints of Approximated Functions (Invited Talk)

Authors: Barbara König

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration. It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions. After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated. We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions. We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints. This is joint work with Paolo Baldan, Sebastian Gurke, Tommaso Padoan and Florian Wittbold.
Cite as

Barbara König. Approximating Fixpoints of Approximated Functions (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{konig:LIPIcs.CSL.2024.4,
  author =	{K\"{o}nig, Barbara},
  title =	{{Approximating Fixpoints of Approximated Functions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello 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.CSL.2024.4},
  URN =		{urn:nbn:de:0030-drops-196469},
  doi =		{10.4230/LIPIcs.CSL.2024.4},
  annote =	{Keywords: fixpoints, approximation, Markov decision processes}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.7
A Lattice-Theoretical View of Strategy Iteration

Authors: Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan

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

Abstract
Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min- respectively max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata.
Cite as

Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. A Lattice-Theoretical View of Strategy Iteration. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CSL.2023.7,
  author =	{Baldan, Paolo and Eggert, Richard and K\"{o}nig, Barbara and Padoan, Tommaso},
  title =	{{A Lattice-Theoretical View of Strategy Iteration}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{7:1--7:19},
  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.7},
  URN =		{urn:nbn:de:0030-drops-174680},
  doi =		{10.4230/LIPIcs.CSL.2023.7},
  annote =	{Keywords: games, strategy iteration, fixpoints, energy games, behavioural metrics}
}
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.FSTTCS.2020.38
Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks

Authors: Rebecca Bernemann, Benjamin Cabrera, Reiko Heckel, and Barbara König

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
This paper exploits extended Bayesian networks for uncertainty reasoning on Petri nets, where firing of transitions is probabilistic. In particular, Bayesian networks are used as symbolic representations of probability distributions, modelling the observer’s knowledge about the tokens in the net. The observer can study the net by monitoring successful and failed steps. An update mechanism for Bayesian nets is enabled by relaxing some of their restrictions, leading to modular Bayesian nets that can conveniently be represented and modified. As for every symbolic representation, the question is how to derive information - in this case marginal probability distributions - from a modular Bayesian net. We show how to do this by generalizing the known method of variable elimination. The approach is illustrated by examples about the spreading of diseases (SIR model) and information diffusion in social networks. We have implemented our approach and provide runtime results.
Cite as

Rebecca Bernemann, Benjamin Cabrera, Reiko Heckel, and Barbara König. Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bernemann_et_al:LIPIcs.FSTTCS.2020.38,
  author =	{Bernemann, Rebecca and Cabrera, Benjamin and Heckel, Reiko and K\"{o}nig, Barbara},
  title =	{{Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{38:1--38:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.38},
  URN =		{urn:nbn:de:0030-drops-132794},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.38},
  annote =	{Keywords: uncertainty reasoning, probabilistic knowledge, Petri nets, Bayesian networks}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.25
Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations

Authors: Paolo Baldan, Barbara König, and Tommaso Padoan

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express many verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract interpretation: a system over some concrete domain is abstracted to a system in a suitable abstract domain, with conditions ensuring that the abstract solution represents a sound/complete overapproximation of the concrete solution. Interestingly, up-to techniques, a classical approach used in coinductive settings to obtain easier or feasible proofs, can be interpreted as abstractions in a way that they naturally fit into our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can characterise the solution of systems of fixpoint equations over complete lattices in terms of a suitable parity game, generalising some recent work that was restricted to continuous lattices. The game view opens the way for the development of local algorithms for characterising the solution of such equation systems and we explore some special cases.
Cite as

Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CONCUR.2020.25,
  author =	{Baldan, Paolo and K\"{o}nig, Barbara and Padoan, Tommaso},
  title =	{{Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.25},
  URN =		{urn:nbn:de:0030-drops-128373},
  doi =		{10.4230/LIPIcs.CONCUR.2020.25},
  annote =	{Keywords: fixpoint equation systems, complete lattices, parity games, abstract interpretation, up-to techniques, \mu-calculus, bisimilarity}
}
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}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.17
Up-To Techniques for Behavioural Metrics via Fibrations

Authors: Filippo Bonchi, Barbara König, and Daniela Petrisan

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.
Cite as

Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2018.17,
  author =	{Bonchi, Filippo and K\"{o}nig, Barbara and Petrisan, Daniela},
  title =	{{Up-To Techniques for Behavioural Metrics via Fibrations}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17},
  URN =		{urn:nbn:de:0030-drops-95552},
  doi =		{10.4230/LIPIcs.CONCUR.2018.17},
  annote =	{Keywords: behavioural metrics, bisimilarity, up-to techniques, coalgebras, fibrations}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.27
Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks

Authors: Benjamin Cabrera, Tobias Heindel, Reiko Heckel, and Barbara König

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
The paper extends Bayesian networks (BNs) by a mechanism for dynamic changes to the probability distributions represented by BNs. One application scenario is the process of knowledge acquisition of an observer interacting with a system. In particular, the paper considers condition/event nets where the observer's knowledge about the current marking is a probability distribution over markings. The observer can interact with the net to deduce information about the marking by requesting certain transitions to fire and observing their success or failure. Aiming for an efficient implementation of dynamic changes to probability distributions of BNs, we consider a modular form of networks that form the arrows of a free PROP with a commutative comonoid structure, also known as term graphs. The algebraic structure of such PROPs supplies us with a compositional semantics that functorially maps BNs to their underlying probability distribution and, in particular, it provides a convenient means to describe structural updates of networks.
Cite as

Benjamin Cabrera, Tobias Heindel, Reiko Heckel, and Barbara König. Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cabrera_et_al:LIPIcs.CONCUR.2018.27,
  author =	{Cabrera, Benjamin and Heindel, Tobias and Heckel, Reiko and K\"{o}nig, Barbara},
  title =	{{Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.27},
  URN =		{urn:nbn:de:0030-drops-95659},
  doi =		{10.4230/LIPIcs.CONCUR.2018.27},
  annote =	{Keywords: Petri nets, Bayesian networks, Probabilistic databases, Condition/Event nets, Probabilistic knowledge, Dynamic probability distributions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.37
(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras

Authors: Barbara König and Christina Mika-Michalski

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics). Our first contribution is to introduce a spoiler-defender bisimulation game for coalgebras in the classical case. Second, we introduce such games for the metric case and furthermore define a real-valued modal coalgebraic logic, from which we can derive the strategy of the spoiler. For this logic we show a quantitative version of the Hennessy-Milner theorem.
Cite as

Barbara König and Christina Mika-Michalski. (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{konig_et_al:LIPIcs.CONCUR.2018.37,
  author =	{K\"{o}nig, Barbara and Mika-Michalski, Christina},
  title =	{{(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.37},
  URN =		{urn:nbn:de:0030-drops-95757},
  doi =		{10.4230/LIPIcs.CONCUR.2018.37},
  annote =	{Keywords: coalgebra, bisimulation games, spoiler-defender games, behavioural metrics, modal logic}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CALCO.2017
LIPIcs, Volume 72, CALCO'17, Complete Volume

Authors: Filippo Bonchi and Barbara König

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

Abstract
LIPIcs, Volume 72, CALCO'17, Complete Volume
Cite as

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{bonchi_et_al:LIPIcs.CALCO.2017,
  title =	{{LIPIcs, Volume 72, CALCO'17, Complete Volume}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  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},
  URN =		{urn:nbn:de:0030-drops-82059},
  doi =		{10.4230/LIPIcs.CALCO.2017},
  annote =	{Keywords: Theory of Computation, Models of computation, Logics and Meanings of Programs, Semantics of Programming Languages – Algebraic Approach}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CALCO.2017.0
Front Matter, Table of Contents, Preface, List of Authors

Authors: Filippo Bonchi and Barbara König

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

Abstract
Front Matter, Table of Contents, Preface, List of Authors
Cite as

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2017.0,
  author =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  title =	{{Front Matter, Table of Contents, Preface, List of Authors}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{0:i--0:x},
  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.0},
  URN =		{urn:nbn:de:0030-drops-80284},
  doi =		{10.4230/LIPIcs.CALCO.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, List of Authors}
}
Document
DOI: 10.4230/DagRep.5.11.1
Verification of Evolving Graph Structures (Dagstuhl Seminar 15451)

Authors: Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)

Abstract
This report documents the programme and the outcome of Dagstuhl Seminar 15451 "Verification of Evolving Graph Structures". The aim was to bring together researchers from different communities (shape analysis, separation logic, graph transformation, verification of infinite-state systems) who are interested in developing techniques for the analysis of graph manipulations, i.e., methods that are able to handle the challenges that arise in current verification problems. Apart from scientific talks, the programme also included four tutorial talks and four working groups, which are summarized in this report.
Cite as

Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis. Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). In Dagstuhl Reports, Volume 5, Issue 11, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{azizabdulla_et_al:DagRep.5.11.1,
  author =	{Aziz Abdulla, Parosh and Gadducci, Fabio and K\"{o}nig, Barbara and Vafeiadis, Viktor},
  title =	{{Verification of Evolving Graph Structures (Dagstuhl Seminar 15451)}},
  pages =	{1--28},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{Aziz Abdulla, Parosh and Gadducci, Fabio and K\"{o}nig, Barbara and Vafeiadis, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.11.1},
  URN =		{urn:nbn:de:0030-drops-57614},
  doi =		{10.4230/DagRep.5.11.1},
  annote =	{Keywords: dynamic systems, graph transformation, graphs, heap analysis, separation logic, shape analysis, static analysis, verification}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.35
Towards Trace Metrics via Functor Lifting

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, by identifying conditions under which also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra in Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.
Cite as

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Towards Trace Metrics via Functor Lifting. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 35-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CALCO.2015.35,
  author =	{Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara},
  title =	{{Towards Trace Metrics via Functor Lifting}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{35--49},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.35},
  URN =		{urn:nbn:de:0030-drops-55254},
  doi =		{10.4230/LIPIcs.CALCO.2015.35},
  annote =	{Keywords: trace metric, monad lifting, pseudometric, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.403
Behavioral Metrics via Functor Lifting

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha : X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states. A first crucial step is the lifting of the functor F on Set to a functor /F in the category PMet of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. Then a final coalgebra for F in Set can be endowed with a behavioral distance resulting as the smallest solution of a fixed-point equation, yielding the final /F-coalgebra in PMet. The same technique, applied to an arbitrary coalgebra alpha : X -> FX in Set, provides the behavioral distance on X. Under some constraints we can prove that two states are at distance 0 if and only if they are behaviorally equivalent.
Cite as

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 403-415, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.FSTTCS.2014.403,
  author =	{Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara},
  title =	{{Behavioral Metrics via Functor Lifting}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{403--415},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.403},
  URN =		{urn:nbn:de:0030-drops-48599},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.403},
  annote =	{Keywords: behavioral metric, functor lifting, pseudometric, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.101
On the Decidability Status of Reachability and Coverability in Graph Transformation Systems

Authors: Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier, and Jan Stückrath

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We study decidability issues for reachability problems in graph transformation systems, a powerful infinite-state model. For a fixed initial configuration, we consider reachability of an entirely specified configuration and of a configuration that satisfies a given pattern (coverability). The former is a fundamental problem for any computational model, the latter is strictly related to verification of safety properties in which the pattern specifies an infinite set of bad configurations. In this paper we reformulate results obtained, e.g., for context-free graph grammars and concurrency models, such as Petri nets, in the more general setting of graph transformation systems and study new results for classes of models obtained by adding constraints on the form of reduction rules.
Cite as

Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier, and Jan Stückrath. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 101-116, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.RTA.2012.101,
  author =	{Bertrand, Nathalie and Delzanno, Giorgio and K\"{o}nig, Barbara and Sangnier, Arnaud and St\"{u}ckrath, Jan},
  title =	{{On the Decidability Status of Reachability and Coverability in  Graph Transformation Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{101--116},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.101},
  URN =		{urn:nbn:de:0030-drops-34871},
  doi =		{10.4230/LIPIcs.RTA.2012.101},
  annote =	{Keywords: decidability, reachability, graph transformation, coverability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.191
Conditional Reactive Systems

Authors: H. J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
We lift the notion of nested application conditions from graph transformation systems to the general categorical setting of reactive systems as defined by Leifer and Milner. This serves two purposes: first, we enrich the formalism of reactive systems by adding application conditions for rules; second, it turns out that some constructions for graph transformation systems (such as computing weakest preconditions and strongest postconditions and showing local confluence by means of critical pair analysis) can be done very elegantly in the more general setting.
Cite as

H. J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König. Conditional Reactive Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 191-203, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bruggink_et_al:LIPIcs.FSTTCS.2011.191,
  author =	{Bruggink, H. J. Sander and Cauderlier, Rapha\"{e}l and H\"{u}lsbusch, Mathias and K\"{o}nig, Barbara},
  title =	{{Conditional Reactive Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{191--203},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.191},
  URN =		{urn:nbn:de:0030-drops-33257},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.191},
  annote =	{Keywords: reactive systems, graph transformation, graph logic, Hoare triples, critical pair analysis}
}
Document
DOI: 10.4230/DagSemProc.04241.1
04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems

Authors: Barbara König, Ugo Montanari, and Philippa Gardner

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract
Recently there has been a lot of research, combining concepts of process algebra with those of the theory of graph grammars and graph transformation systems. Both can be viewed as general frameworks in which one can specify and reason about concurrent and distributed systems. There are many areas where both theories overlap and this reaches much further than just using graphs to give a graphic representation to processes. Processes in a communication network can be seen in two different ways: as terms in an algebraic theory, emphasizing their behaviour and their interaction with the environment, and as nodes (or edges) in a graph, emphasizing their topology and their connectedness. Especially topology, mobility and dynamic reconfigurations at runtime can be modelled in a very intuitive way using graph transformation. On the other hand the definition and proof of behavioural equivalences is often easier in the process algebra setting. Also standard techniques of algebraic semantics for universal constructions, refinement and compositionality can take better advantage of the process algebra representation. An important example where the combined theory is more convenient than both alternatives is for defining the concurrent (noninterleaving), abstract semantics of distributed systems. Here graph transformations lack abstraction and process algebras lack expressiveness. Another important example is the work on bigraphical reactive systems with the aim of deriving a labelled transitions system from an unlabelled reactive system such that the resulting bisimilarity is a congruence. Here, graphs seem to be a convenient framework, in which this theory can be stated and developed. So, although it is the central aim of both frameworks to model and reason about concurrent systems, the semantics of processes can have a very different flavour in these theories. Research in this area aims at combining the advantages of both frameworks and translating concepts of one theory into the other. The Dagsuthl Seminar, which took place from 06.06. to 11.06.2004, was aimed at bringing together researchers of the two communities in order to share their ideas and develop new concepts. These proceedings4 of the do not only contain abstracts of the talks given at the seminar, but also summaries of topics of central interest. We would like to thank all participants of the seminar for coming and sharing their ideas and everybody who has contributed to the proceedings.
Cite as

Barbara König, Ugo Montanari, and Philippa Gardner. 04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{konig_et_al:DagSemProc.04241.1,
  author =	{K\"{o}nig, Barbara and Montanari, Ugo and Gardner, Philippa},
  title =	{{04241 Abstracts Collection – Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.1},
  URN =		{urn:nbn:de:0030-drops-279},
  doi =		{10.4230/DagSemProc.04241.1},
  annote =	{Keywords: graph transformation , process calculi}
}
Document
DOI: 10.4230/DagSemProc.04241.3
Summary 2: Graph Grammar Verification through Abstraction

Authors: Paolo Baldan, Barbara König, and Arend Rensink

Published in: Dagstuhl Seminar Proceedings, Volume 4241, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems (2005)

Abstract
Until now there have been few contributions concerning the verification of graph grammars, specifically of infinite-state graph grammars. This paper compares two existing approaches, based on abstractions of graph transformation systems. While in the unfolding approach graph grammars are approximated by Petri nets, in the partitioning approach graphs are abstracted according to their local structure. We describe differences and similarities of the two approaches and explain the underlying ideas.
Cite as

Paolo Baldan, Barbara König, and Arend Rensink. Summary 2: Graph Grammar Verification through Abstraction. In Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, Volume 4241, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:DagSemProc.04241.3,
  author =	{Baldan, Paolo and K\"{o}nig, Barbara and Rensink, Arend},
  title =	{{Summary 2: Graph Grammar Verification through Abstraction}},
  booktitle =	{Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4241},
  editor =	{Barbara K\"{o}nig and Ugo Montanari and Philippa Gardner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04241.3},
  URN =		{urn:nbn:de:0030-drops-291},
  doi =		{10.4230/DagSemProc.04241.3},
  annote =	{Keywords: graph transformation , verification}
}
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 Imprint Privacy Contact