Author name cluster

Jurriaan Rot

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

CSL Conference 2026 Conference Paper

Constructing Witnesses for Lower Bounds on Behavioural Distances

Ruben Turkenburg
Harsh Beohar
Franck van Breugel
Clemens Kupke
Jurriaan Rot

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.

Details

FM Conference 2026 Conference Paper

Error-Awareness Accelerates Active Automata Learning

Loes Kruger
Sebastian Junges
Jurriaan Rot

Abstract Active automata learning (AAL) algorithms can learn a behavioral model of a system from interacting with it. The primary challenge remains scaling to larger models, in particular in the presence of many possible inputs to the system. Modern AAL algorithms fail to scale even if, in every state, most inputs lead to errors. In various challenging problems from the literature, these errors are observable, i. e. , they emit a known error output. Motivated by these problems, we study learning these systems more efficiently. Further, we consider various degrees of knowledge about which inputs are non-error producing at which state. For each level of knowledge, we provide a matching adaptation of the state-of-the-art AAL algorithm $$L^{\#}$$ L # to make the most of this domain knowledge. Our empirical evaluation demonstrates that the methods accelerate learning by orders of magnitude with strong but realistic domain knowledge to a single order of magnitude with limited domain knowledge.

DOI

CSL Conference 2025 Conference Paper

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

Samuel Humeau 0002
Daniela Petrisan
Jurriaan Rot

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.

Details

TCS Journal 2022 Journal Article

Fast computations on ordered nominal sets

David Venhoek
Joshua Moerman
Jurriaan Rot

Nominal automata are models for recognising languages over infinite alphabets, based on the algebraic notion of nominal set. Motivated by their use in automata theory, we show how to compute efficiently with nominal sets over the so-called total order symmetry, a variant which allows to compare alphabet letters for equality as well as their respective order. We develop an explicit finite representation of such nominal sets and basic constructions thereon. The approach is implemented as the library Ons (Ordered Nominal Sets), enabling programming with infinite sets. Returning to our motivation of nominal automata, we evaluate Ons in two applications: minimisation of automata and active automata learning. In both cases, Ons is competitive compared to existing implementations and outperforms them for certain classes of inputs.

Details DOI

CSL Conference 2020 Conference Paper

Expressive Logics for Coinductive Predicates

Clemens Kupke
Jurriaan Rot

The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.

Details

MFCS Conference 2020 Conference Paper

Preservation of Equations by Monoidal Monads

Louis Parlant
Jurriaan Rot
Alexandra Silva 0001
Bas Westerbaan

If a monad T is monoidal, then operations on a set X can be lifted canonically to operations on TX. In this paper we study structural properties under which T preserves equations between those operations. It has already been shown that any monoidal monad preserves linear equations; affine monads preserve drop equations (where some variable appears only on one side, such as x⋅ y = y) and relevant monads preserve dup equations (where some variable is duplicated, such as x ⋅ x = x). We start the paper by showing a converse: if the monad at hand preserves a drop equation, then it must be affine. From this, we show that the problem whether a given (drop) equation is preserved is undecidable. A converse for relevance turns out to be more subtle: preservation of certain dup equations implies a weaker notion which we call n-relevance. Finally, we identify a subclass of equations such that their preservation is equivalent to relevance.

Details

CSL Conference 2020 Conference Paper

Separation and Renaming in Nominal Sets

Joshua Moerman
Jurriaan Rot

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e. g. , to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Details

I&C Journal 2016 Journal Article

Proving language inclusion and equivalence by coinduction

Jurriaan Rot
Marcello Bonsangue
Jan Rutten

Language equivalence and inclusion can be checked coinductively by establishing a (bi)simulation on suitable deterministic automata. In this paper we present an enhancement of this technique called (bi)simulation-up-to. We give general conditions on language operations for which bisimulation-up-to is sound. These results are illustrated by a large number of examples, giving new proofs of classical results such as Arden's rule, and involving the regular operations of union, concatenation and Kleene star as well as language equations with complement and intersection, and shuffle (closure).

Details DOI

Highlights Conference 2014 Conference Abstract

Coinduction-up-to

Jurriaan Rot

Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. The use of such techniques dates back to Milner's initial work on bisimilarity. Since then, coinduction up-to proved useful, if not essential, in numerous proofs about concurrent systems; it has been used to obtain decidability results, and more recently to improve standard automata algorithms. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modelled as coalgebras. By tuning the parameters of our framework, we obtain novel techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity. This is joint work with Filippo Bonchi, Daniela Petrisan and Damien Pous. 11: 45 12: 00 Break

PDF Details