40 citations · 156 across the 43 of their papers we have counts for
37 papers · 1 filter
GKAT with Hoare Hypotheses
Jurriaan Rot, Todd Schmid, Jana Wagemaker
Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for pro…
Initial Algebra Correspondence under Reachability Conditions
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot
Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Mark…
Constructing Witnesses for Lower Bounds on Behavioural Distances
Ruben Turkenburg, Harsh Beohar, Franck van Breugel +2
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 f…
Trees in Coalgebra from Generalized Reachability
Thorsten Wißmann, Bálint Kocsis, Jurriaan Rot +1
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 o…
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot +1
The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between f…
Relating Apartness and Branching Bisimulation Games
Jurriaan Rot, Sebastian Junges, Harsh Beohar
Geuvers and Jacobs (LMCS 2021) formulated the notion of apartness relation on state-based systems modelled as coalgebras. In this context apartness is formally dual to bisimilarity…
Relational Connectors and Heterogeneous Bisimulations
Pedro Nora, Jurriaan Rot, Lutz Schröder +1
While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of…
A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Kazuki Watanabe, Sebastian Junges, Jurriaan Rot +1
Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temp…
State Matching and Multiple References in Adaptive Active Automata Learning
Loes Kruger, Sebastian Junges, Jurriaan Rot
Active automata learning (AAL) is a method to infer state machines by interacting with black-box systems. Adaptive AAL aims to reduce the sample complexity of AAL by incorporating…
Composing Codensity Bisimulations
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot +1
Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical for…
A Categorical Approach to Coalgebraic Fixpoint Logic
Ezra Schoen, Clemens Kupke, Jurriaan Rot +1
We define a framework for incorporating alternation-free fixpoint logics into the dual-adjunction setup for coalgebraic modal logics. We achieve this by using order-enriched catego…
Proving Behavioural Apartness
Ruben Turkenburg, Harsh Beohar, Clemens Kupke +1
Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yi…
Small Test Suites for Active Automata Learning
Loes Kruger, Sebastian Junges, Jurriaan Rot
A bottleneck in modern active automata learning is to test whether a hypothesized Mealy machine correctly describes the system under learning. The search space for possible counter…
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo +2
Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally de…
Processes Parametrised by an Algebraic Theory
Todd Schmid, Wojciech Rozowski, Alexandra Silva +1
We develop a (co)algebraic framework to study a family of process calculi with monadic branching structures and recursion operators. Our framework features a uniform semantics of p…
On Star Expressions and Coalgebraic Completeness Theorems
Todd Schmid, Jurriaan Rot, Alexandra Silva
An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete.…
Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation
Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke +2
A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (proba…
Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics
Ornela Dardha, Jurriaan Rot
This volume contains the proceedings of EXPRESS/SOS 2020: the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational…
Partially Observable Concurrent Kleene Algebra
Jana Wagemaker, Paul Brunet, Simon Docherty +3
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and lo…
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…
Steps and Traces
Jurriaan Rot, Bart Jacobs, Paul Levy
In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg-Moore cat…
Up-to Techniques for Branching Bisimilarity
Rick Erkens, Jurriaan Rot, Bas Luttik
Ever since the introduction of behavioral equivalences on processes one has been searching for efficient proof techniques that accompany those equivalences. Both strong bisimilarit…
Preservation of Equations by Monoidal Monads
Louis Parlant, Jurriaan Rot, Alexandra Silva +1
If a monad is monoidal, then operations on a set can be lifted canonically to operations on . In this paper we study structural properties under which preserves equ…
Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics
Jorge A. Pérez, Jurriaan Rot
This volume contains the proceedings of EXPRESS/SOS 2019: the Combined 26th International Workshop on Expressiveness in Concurrency and the 16th Workshop on Structural Operational…