DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2026.25

Constructing Witnesses for Lower Bounds on Behavioural Distances

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

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

Behavioural distances provide a robust alternative to notions of equivalence such as bisimilarity in the context of probabilistic transition systems. They can be defined as least fixed points, whose universal property allows us to exhibit upper bounds on the distance between states, showing them to be at most some distance apart. In this paper, we instead consider the problem of bounding distances from below, showing states to be at least some distance apart. Contrary to upper bounds, it is possible to reason about lower bounds inductively. We exploit this by giving an inductive derivation system for lower bounds on an existing definition of behavioural distance for labelled Markov chains. This is inspired by recent work on apartness as an inductive counterpart to bisimilarity. Proofs in our system will be shown to closely match the behavioural distance by soundness and (approximate) completeness results. We further provide a constructive correspondence between our derivation system and formulas in a modal logic with quantitative semantics. This logic was used in recent work of Rady and van Breugel to construct evidence for lower bounds on behavioural distances. Our constructions provide smaller witnessing formulas in many examples.

Cite as

Ruben Turkenburg, Harsh Beohar, Franck van Breugel, Clemens Kupke, and Jurriaan Rot. Constructing Witnesses for Lower Bounds on Behavioural Distances. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{turkenburg_et_al:LIPIcs.CSL.2026.25,
  author =	{Turkenburg, Ruben and Beohar, Harsh and van Breugel, Franck and Kupke, Clemens and Rot, Jurriaan},
  title =	{{Constructing Witnesses for Lower Bounds on Behavioural Distances}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{25:1--25:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.25},
  URN =		{urn:nbn:de:0030-drops-254493},
  doi =		{10.4230/LIPIcs.CSL.2026.25},
  annote =	{Keywords: Behavioural Distances, Markov Chains, Apartness}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.26

ε-Distance via Lévy-Prokhorov Lifting

Authors: Josée Desharnais and Ana Sokolova

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics. Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute. We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.

Cite as

Josée Desharnais and Ana Sokolova. ε-Distance via Lévy-Prokhorov Lifting. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 26:1-26:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.CSL.2026.26,
  author =	{Desharnais, Jos\'{e}e and Sokolova, Ana},
  title =	{{\epsilon-Distance via L\'{e}vy-Prokhorov Lifting}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{26:1--26:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.26},
  URN =		{urn:nbn:de:0030-drops-254506},
  doi =		{10.4230/LIPIcs.CSL.2026.26},
  annote =	{Keywords: L\'{e}vy-Prokhorov metric, behavioural distance, epsilon-bisimulation, reactive probabilistic transition systems, discrete labelled Markov processes, coalgebraic epsilon-(bi)simulation}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2025.14

Register Automata with Permutations

Authors: Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, and Nikos Tzevelekos

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract

We propose Permutation Deterministic Register Automata (pDRAs), a deterministic register automaton model where we allow permutations of registers in transitions. The model enables minimal canonical representations and pDRAs can be tested for equivalence in polynomial time. The complexity of minimization is between GI (the complexity of graph isomorphism) and NP. We then introduce a subclass of pDRAs, called register automata with fixed permutation policy, where the register permutation discipline is stipulated globally. This class generalizes the model proposed by Benedikt, Ley and Puppis in 2010, and we show that it also admits minimal and canonical representations, based on a finite-index word equivalence relation. As an application, we show that for any regular data language L, the minimal register automaton with fixed permutation policy recognizing L can be actively learned in polynomial time using oracles for membership, equivalence and data-memorability queries. We show that all the oracles can be implemented in polynomial time, and so this yields a polynomial time minimization algorithm.

Cite as

Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, and Nikos Tzevelekos. Register Automata with Permutations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{balachander_et_al:LIPIcs.MFCS.2025.14,
  author =	{Balachander, Mrudula and Filiot, Emmanuel and Gentilini, Raffaella and Tzevelekos, Nikos},
  title =	{{Register Automata with Permutations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.14},
  URN =		{urn:nbn:de:0030-drops-241219},
  doi =		{10.4230/LIPIcs.MFCS.2025.14},
  annote =	{Keywords: Register automata, data words, equivalence, minimization, active learning}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.20

Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement

Authors: Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. We characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We present a compositional learning algorithm implementing these ideas, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments show that in more than 630 subject systems, CoalA delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.

Cite as

Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino. Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henry_et_al:LIPIcs.CONCUR.2025.20,
  author =	{Henry, L\'{e}o and Mousavi, Mohammad Reza and Neele, Thomas and Sammartino, Matteo},
  title =	{{Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{20:1--20:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.20},
  URN =		{urn:nbn:de:0030-drops-239700},
  doi =		{10.4230/LIPIcs.CONCUR.2025.20},
  annote =	{Keywords: Active learning, Compositional methods, Concurrency theory, Labelled transition systems, Formal methods}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.34

New Fault Domains for Conformance Testing of Finite State Machines

Authors: Frits Vaandrager and Ivo Melse

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

A fault domain reflects a tester’s assumptions about faults that may occur in an implementation and that need to be detected during testing. A fault domain that has been widely studied in the literature on black-box conformance testing is the class of finite state machines (FSMs) with at most m states. Numerous strategies for generating test suites have been proposed that guarantee fault coverage for this class. These so-called m-complete test suites grow exponentially in m-n, where n is the number of states of the specification, so one can only run them for small values of m-n. But the assumption that m-n is small is not realistic in practice. In his seminal paper from 1964, Hennie raised the challenge to design checking experiments in which the number of states may increase appreciably. In order to solve this long-standing open problem, we propose (much larger) fault domains that capture the assumption that all states in an implementation can be reached by first performing a sequence from some set A (typically a state cover for the specification), followed by k arbitrary inputs, for some small k. The number of states of FSMs in these fault domains grows exponentially in k. We present a sufficient condition for k-A-completeness of test suites with respect to these fault domains. Our condition implies k-A-completeness of two prominent m-complete test suite generation strategies, the Wp and HSI methods. Thus these strategies are complete for much larger fault domains than those for which they were originally designed, and thereby solve Hennie’s challenge. We show that three other prominent m-complete methods (H, SPY and SPYH) do not always generate k-A-complete test suites.

Cite as

Frits Vaandrager and Ivo Melse. New Fault Domains for Conformance Testing of Finite State Machines. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vaandrager_et_al:LIPIcs.CONCUR.2025.34,
  author =	{Vaandrager, Frits and Melse, Ivo},
  title =	{{New Fault Domains for Conformance Testing of Finite State Machines}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{34:1--34:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.34},
  URN =		{urn:nbn:de:0030-drops-239843},
  doi =		{10.4230/LIPIcs.CONCUR.2025.34},
  annote =	{Keywords: conformance testing, finite state machines, Mealy machines, apartness, observation tree, fault domains, k-A-complete test suites}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.36

Explainability is a Game for Probabilistic Bisimilarity Distances

Authors: Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

We revisit a game from the literature that characterizes the probabilistic bisimilarity distances of a labelled Markov chain. We illustrate how an optimal policy of the game can explain these distances. Like the games that characterize bisimilarity and probabilistic bisimilarity, the game is played on pairs of states and matches transitions of those states. To obtain more convincing and interpretable explanations than those provided by generic optimal policies, we restrict to optimal policies that delay reaching observably inequivalent state pairs for as long as possible (called 1-maximal) while quickly reaching equivalent ones (called 0-minimal). We present iterative algorithms that compute 1-maximal and 0-minimal policies and prove an exponential lower bound for the number of iterations of the algorithm that computes 1-maximal policies.

Cite as

Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a Game for Probabilistic Bisimilarity Distances. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vlasman_et_al:LIPIcs.CONCUR.2025.36,
  author =	{Vlasman, Emily and Nanah Ji, Anto and Worrell, James and van Breugel, Franck},
  title =	{{Explainability is a Game for Probabilistic Bisimilarity Distances}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.36},
  URN =		{urn:nbn:de:0030-drops-239861},
  doi =		{10.4230/LIPIcs.CONCUR.2025.36},
  annote =	{Keywords: probabilistic bisimilarity distance, labelled Markov chain, game, policy, explainability}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2025.14

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Authors: Kazuki Watanabe

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract

Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure. Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.

Cite as

Kazuki Watanabe. Pareto Fronts for Compositionally Solving String Diagrams of Parity Games. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{watanabe:LIPIcs.CALCO.2025.14,
  author =	{Watanabe, Kazuki},
  title =	{{Pareto Fronts for Compositionally Solving String Diagrams of Parity Games}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.14},
  URN =		{urn:nbn:de:0030-drops-235734},
  doi =		{10.4230/LIPIcs.CALCO.2025.14},
  annote =	{Keywords: parity game, compositionality, string diagram}
}

Document

(Co)algebraic pearl

DOI: 10.4230/LIPIcs.CALCO.2025.16

Active Learning of Upward-Closed Sets of Words ((Co)algebraic pearl)

Authors: Quentin Aristote

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract

We give a new proof of a result from well quasi-order theory on the computability of bases for upwards-closed sets of words. This new proof is based on Angluin’s L* algorithm, that learns an automaton from a minimally adequate teacher. This relates in particular two results from the 1980s: Angluin’s L* algorithm, and a result from Valk and Jantzen on the computability of bases for upwards-closed sets of tuples of integers. Along the way, we describe an algorithm for learning quasi-ordered automata from a minimally adequate teacher, and extend a generalization of Valk and Jantzen’s result, encompassing both words and integers, to finitely generated monoids.

Cite as

Quentin Aristote. Active Learning of Upward-Closed Sets of Words ((Co)algebraic pearl). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 16:1-16:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aristote:LIPIcs.CALCO.2025.16,
  author =	{Aristote, Quentin},
  title =	{{Active Learning of Upward-Closed Sets of Words}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{16:1--16:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.16},
  URN =		{urn:nbn:de:0030-drops-235751},
  doi =		{10.4230/LIPIcs.CALCO.2025.16},
  annote =	{Keywords: active learning, well quasi-orders, Valk-Jantzen lemma, piecewise-testable languages, monoids}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2025.13

Expressivity of Bisimulation Pseudometrics over Analytic State Spaces

Authors: Daniel Luckhardt, Harsh Beohar, and Clemens Kupke

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract

A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of measurable spaces. Note that analytic spaces were already studied in the literature on labelled Markov processes and bisimulation relations. Our results are twofold. First, we define bisimulation pseudometrics over such coalgebras using the framework of fibrations. Second, we develop a quantitative modal logic for such coalgebras and prove a quantitative form of Hennessy-Milner theorem in this new setting stating that the bisimulation pseudometric corresponds to the logical distance induced by modal formulae.

Cite as

Daniel Luckhardt, Harsh Beohar, and Clemens Kupke. Expressivity of Bisimulation Pseudometrics over Analytic State Spaces. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{luckhardt_et_al:LIPIcs.CALCO.2025.13,
  author =	{Luckhardt, Daniel and Beohar, Harsh and Kupke, Clemens},
  title =	{{Expressivity of Bisimulation Pseudometrics over Analytic State Spaces}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{13:1--13:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.13},
  URN =		{urn:nbn:de:0030-drops-235727},
  doi =		{10.4230/LIPIcs.CALCO.2025.13},
  annote =	{Keywords: Markov decision process, quantitative Hennessy-Milner theorem}
}

Document

(Co)algebraic pearl

DOI: 10.4230/LIPIcs.CALCO.2025.15

Trees in Coalgebra from Generalized Reachability ((Co)algebraic pearl)

Authors: Thorsten Wißmann, Bálint Kocsis, Jurriaan Rot, and Ruben Turkenburg

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract

An automaton is called reachable if every state is reachable from the initial state. This notion has been generalized coalgebraically in two ways: first, via a universal property on pointed coalgebras, namely, that a reachable coalgebra has no proper subcoalgebra; and second, a coalgebra is reachable if it arises as the union of an iterative computation of successor states, starting from the initial state. In the current paper, we present corresponding universal properties and iterative constructions for trees. The universal property captures when a coalgebra is a tree, namely, when it has no proper tree unravelling. The iterative construction unravels an arbitrary coalgebra to a tree. We show that this yields the expected notion of tree for a variety of standard examples. We obtain our characterization of trees by first generalizing the previous theory of reachable coalgebras. Surprisingly, both the universal property and the iterative construction for trees arise as an instance of this generalized notion of reachability.

Cite as

Thorsten Wißmann, Bálint Kocsis, Jurriaan Rot, and Ruben Turkenburg. Trees in Coalgebra from Generalized Reachability ((Co)algebraic pearl). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{wimann_et_al:LIPIcs.CALCO.2025.15,
  author =	{Wi{\ss}mann, Thorsten and Kocsis, B\'{a}lint and Rot, Jurriaan and Turkenburg, Ruben},
  title =	{{Trees in Coalgebra from Generalized Reachability}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.15},
  URN =		{urn:nbn:de:0030-drops-235740},
  doi =		{10.4230/LIPIcs.CALCO.2025.15},
  annote =	{Keywords: Trees, Coalgebra, Factorization Systems}
}

Document

DOI: 10.4230/DagRep.14.10.58

Behavioural Metrics and Quantitative Logics (Dagstuhl Seminar 24432)

Authors: Barbara König, Radu Mardare, Prakash Panangaden, Jurriaan Rot, and Florence Clerc

Published in: Dagstuhl Reports, Volume 14, Issue 10 (2025)

Abstract

This report documents the program and the outcome of Dagstuhl Seminar "Behavioural Metrics and Quantitative Logics" (24432). Behavioural metrics and quantitative logics specify quantitative aspects of systems. A metric measures how far apart two systems are in their behaviour while a quantititative logic evaluates the degree to which a state satisfies a formula. They are often intimately connected via a Hennessy-Milner theorem stating that the distance induced by a quantitative logic coincides with behavioural distance. There are various applications in model-checking, differential privacy, hybrid systems and learning. Several challenges in this area have been identified: studying suitable metrics and their corresponding logics, generalizing to the setting of coalgebras by parameterizing the branching type of the system under consideration, developing methods of quantitative algebraic reasoning, finding efficient methods for computing behavioural methods. This Dagstuhl Seminar provided a forum to researchers working in this area, to discuss the state-of-the-art and further developments, and in particular address applications in various domains.

Cite as

Barbara König, Radu Mardare, Prakash Panangaden, Jurriaan Rot, and Florence Clerc. Behavioural Metrics and Quantitative Logics (Dagstuhl Seminar 24432). In Dagstuhl Reports, Volume 14, Issue 10, pp. 58-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{konig_et_al:DagRep.14.10.58,
  author =	{K\"{o}nig, Barbara and Mardare, Radu and Panangaden, Prakash and Rot, Jurriaan and Clerc, Florence},
  title =	{{Behavioural Metrics and Quantitative Logics (Dagstuhl Seminar 24432)}},
  pages =	{58--75},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{14},
  number =	{10},
  editor =	{K\"{o}nig, Barbara and Mardare, Radu and Panangaden, Prakash and Rot, Jurriaan and Clerc, Florence},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.10.58},
  URN =		{urn:nbn:de:0030-drops-230222},
  doi =		{10.4230/DagRep.14.10.58},
  annote =	{Keywords: Behavioural metrics, quantitative equational reasoning, quantitative logics}
}

Document

DOI: 10.4230/LIPIcs.STACS.2025.40

Identity-Preserving Lax Extensions and Where to Find Them

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract

Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.

Cite as

Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Identity-Preserving Lax Extensions and Where to Find Them. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.STACS.2025.40,
  author =	{Goncharov, Sergey and Hofmann, Dirk and Nora, Pedro and Schr\"{o}der, Lutz and Wild, Paul},
  title =	{{Identity-Preserving Lax Extensions and Where to Find Them}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{40:1--40:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.40},
  URN =		{urn:nbn:de:0030-drops-228665},
  doi =		{10.4230/LIPIcs.STACS.2025.40},
  annote =	{Keywords: (Bi-)simulations, lax extensions, modal logics, coalgebra}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.28

Strong Induction Is an Up-To Technique

Authors: Filippo Bonchi, Elena Di Lavore, and Anna Ricci

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion.

Cite as

Filippo Bonchi, Elena Di Lavore, and Anna Ricci. Strong Induction Is an Up-To Technique. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2025.28,
  author =	{Bonchi, Filippo and Di Lavore, Elena and Ricci, Anna},
  title =	{{Strong Induction Is an Up-To Technique}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.28},
  URN =		{urn:nbn:de:0030-drops-227856},
  doi =		{10.4230/LIPIcs.CSL.2025.28},
  annote =	{Keywords: Induction, Coinduction, Up-to Techniques, Induction up-to, Lattices, Algebras}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.29

Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach

Authors: Samuel Humeau, Daniela Petrisan, and Jurriaan Rot

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

The Kantorovich distance is a widely used metric between probability distributions. The Kantorovich-Rubinstein duality states that it can be defined in two equivalent ways: as a supremum, based on non-expansive functions into [0,1], and as an infimum, based on probabilistic couplings. Orthogonally, there are categorical generalisations of both presentations proposed in the literature, in the form of codensity liftings and what we refer to as coupling-based liftings. Both lift endofunctors on the category Set of sets and functions to that of pseudometric spaces, and both are parameterised by modalities from coalgebraic modal logic. A generalisation of the Kantorovich-Rubinstein duality has been more nebulous - it is known not to work in some cases. In this paper we propose a compositional approach for obtaining such generalised dualities for a class of functors, which is closed under coproducts and products. Our approach is based on an explicit construction of modalities and also applies to and extends known cases such as that of the powerset functor.

Cite as

Samuel Humeau, Daniela Petrisan, and Jurriaan Rot. Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{humeau_et_al:LIPIcs.CSL.2025.29,
  author =	{Humeau, Samuel and Petrisan, Daniela and Rot, Jurriaan},
  title =	{{Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.29},
  URN =		{urn:nbn:de:0030-drops-227861},
  doi =		{10.4230/LIPIcs.CSL.2025.29},
  annote =	{Keywords: Kantorovich distance, behavioural metrics, Kantorovich-Rubinstein duality, functor liftings}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.33

Quantitative Graded Semantics and Spectra of Behavioural Metrics

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

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/ branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.

Cite as

Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Quantitative Graded Semantics and Spectra of Behavioural Metrics. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2025.33,
  author =	{Forster, Jonas and Schr\"{o}der, Lutz and Wild, Paul and Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla},
  title =	{{Quantitative Graded Semantics and Spectra of Behavioural Metrics}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.33},
  URN =		{urn:nbn:de:0030-drops-227907},
  doi =		{10.4230/LIPIcs.CSL.2025.33},
  annote =	{Keywords: transition systems, modal logics, coalgebras, behavioural metrics}
}

32 Search Results for "Rot, Jurriaan"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message