SU\G(𝔸)/K·U
Sign Up for free Log In

Author Description

Login to generate an author description

Ask a Question About This Mathematician

Coinduction up-to in a fibrational setting

2014-07-14
Filippo Bonchi , Daniela Petrişan , Damien Pous +1 more
Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a … Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. 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.
View PDF Chat

Presenting Distributive Laws

2013-01-01
Marcello Bonsangue , Helle Hvid Hansen , Alexander Kurz +1 more
View PDF Chat

Presenting Distributive Laws

2015-08-07
Marcello Bonsangue , Helle Hvid Hansen , Alexander Kurz +1 more
Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the … Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages.
View PDF Chat

Coalgebraic trace semantics via forgetful logics

2017-04-27
Bartek Klin , Jurriaan Rot
We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and … We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition under which a logical semantics coincides with the trace semantics obtained via a given determinization construction. Finally, we consider a condition that guarantees the existence of a canonical determinization procedure that is correct with respect to a given logical semantics. That procedure is closely related to Brzozowski's minimization algorithm.
View PDF Chat

Expressivity of Quantitative Modal Logics : Categorical Foundations via Codensity and Approximation

2021-06-29
Yuichi Komorida , Shin-ya Katsumata , Clemens Kupke +2 more
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 (probabilistic, … 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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting-a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by König et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.
View PDF Chat

Learning Pomset Automata

2021-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +1 more
View PDF Chat

Expressive Logics for Coinductive Predicates

2021-12-15
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 … 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.
View PDF Chat

On the specification of operations on the rational behaviour of systems

2012-08-12
Marcello Bonsangue , Stefan Milius , Jurriaan Rot
Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields specification formats for well-behaved algebraic operations on final coalgebras, which are … Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields specification formats for well-behaved algebraic operations on final coalgebras, which are a domain for the behaviour of all systems of a given type functor. We introduce a format for specification of algebraic operations that restrict to the rational fixpoint of a functor, which captures the behaviour of finite systems. In other words, we show that rational behaviour is closed under operations specified in our format. As applications we consider operations on regular languages, regular processes and finite weighted transition systems.
View PDF Chat

Interacting via the Heap in the Presence of Recursion

2012-12-14
Jurriaan Rot , Irina Măriuca Asăvoae , Frank de Boer +2 more
Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive … Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive procedures and local variables the interactions of a program with the heap can become rather complex, as an unbounded number of objects can be allocated either on the call stack using local variables, or, anonymously, on the heap using reference fields. As such a static analysis is, in general, undecidable. In this paper we study the verification of recursive programs with unbounded allocation of objects, in a simple imperative language for heap manipulation. We present an improved semantics for this language, using an abstraction that is precise. For any program with a bounded visible heap, meaning that the number of objects reachable from variables at any point of execution is bounded, this abstraction is a finitary representation of its behaviour, even though an unbounded number of objects can appear in the state. As a consequence, for such programs model checking is decidable. Finally we introduce a specification language for temporal properties of the heap, and discuss model checking these properties against heap-manipulating programs.
View PDF Chat

Coalgebraic Determinization of Alternating Automata.

2018-04-07
Meven Bertrand , Jurriaan Rot
Coalgebra is a currently quite active field, which aims to look at generic state-based systems (most prominently automata) from a very abstract point of view, mainly using tools from category … Coalgebra is a currently quite active field, which aims to look at generic state-based systems (most prominently automata) from a very abstract point of view, mainly using tools from category theory. One of its achievements is to give a completely generic approach of determinization, unifying in an elegant manner non-deterministic automata, probabilistic automata or non-deterministic pushdown automata in one and the same model. However, the case of alternating automata fails to easily fit in this model. The aim of this internship was therefore to tackle this problem: can alternating automata also be determinized in the coalgebraic way? Does this give semantics that coincides with the concretely defined one? In this report, we give a positive answer to both questions. The main element of our construction is a distributive law, the definition of which has been for some time an open question.

Steps and Traces

2018-01-01
Bart Jacobs , Paul Blain Levy , Jurriaan Rot
View PDF Chat

Duality of Equations and Coequations via Contravariant Adjunctions

2016-01-01
Julian Salamanca , Marcello Bonsangue , Jurriaan Rot
View PDF Chat

Partially Observable Concurrent Kleene Algebra

2020-01-01
Jana Wagemaker , Paul Brunet , Simon Docherty +3 more
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that … We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.
View PDF Chat

Steps and traces

2021-07-14
Jurriaan Rot , Bart Jacobs , Paul Blain Levy
Abstract 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 category. This … Abstract 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 category. This paper elaborates two new unifying ideas: (i) coalgebraic,draftrules trace semantics is naturally presented in terms of corecursive algebras, and (ii) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof and allows to derive conditions under which some of them coincide.
View PDF Chat

Concurrent NetKAT

2022-01-01
Jana Wagemaker , Nate Foster , Tobias Kappé +3 more
We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. We provide a model of … We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. We provide a model of the language based on partially-ordered multisets (pomsets), which are a well-established mathematical structure for defining the denotational semantics of concurrent languages. We provide a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through examples. More generally, CNetKAT can be understood as an algebraic framework for reasoning about programs with both local state (in packets) and global state (in a global store).
View PDF Chat

Tree Automata as Algebras: Minimisation and Determinisation

2019-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
We study a categorical generalisation of tree automata, as $\Sigma$-algebras for a fixed endofunctor $\Sigma$ endowed with initial and final states. Under mild assumptions about the base category, we present … We study a categorical generalisation of tree automata, as $\Sigma$-algebras for a fixed endofunctor $\Sigma$ endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.

Up-to Techniques for Branching Bisimilarity

2020-01-01
Rick Erkens , Jurriaan Rot , Bas Luttik
View PDF Chat

Distributive Laws for Monotone Specifications

2017-08-31
Jurriaan Rot
Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract … Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications - that disallow negative premises - do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation.
View PDF Chat

Fast Computations on Ordered Nominal Sets

2018-01-01
David Venhoek , Joshua Moerman , Jurriaan Rot
View PDF Chat

Separation and Renaming in Nominal Sets

2019-06-03
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 … 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. These automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Completeness and Incompleteness of Synchronous Kleene Algebra

2019-01-01
Jana Wagemaker , Marcello Bonsangue , Tobias Kappé +2 more
View PDF Chat

Preservation of Equations by Monoidal Monads

2020-01-01
Louis Parlant , Jurriaan Rot , Alexandra Silva +1 more
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 … 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.

On Star Expressions and Completeness Theorems

2021-12-27
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. One … 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. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other.
View PDF Chat

Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics

2020-08-27
Ornela Dardha , Jurriaan Rot
View PDF Chat

A New Approach for Active Automata Learning Based on Apartness

2021-01-01
Frits Vaandrager , Bharat Garhewal , Jurriaan Rot +1 more
We present $L^{\#}$, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $L^{\ast}$ algorithm and its descendants, $L^{\#}$ takes a different … We present $L^{\#}$, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $L^{\ast}$ algorithm and its descendants, $L^{\#}$ takes a different perspective: it tries to establish apartness, a constructive form of inequality. $L^{\#}$ does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. $L^{\#}$ has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of $L^{\#}$ in practice. Experiments with a prototype implementation, written in Rust, suggest that $L^{\#}$ is competitive with existing algorithms.

Fast computations on ordered nominal sets

2022-09-06
David Venhoek , Joshua Moerman , Jurriaan Rot
View PDF Chat

Kleene Algebra with Observations

2018-01-01
Tobias Kappé , Paul Brunet , Jurriaan Rot +3 more
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms … Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.
View PDF Chat

Composing Codensity Bisimulations

2024-06-21
Mayuko Kori , Kazuki Watanabe , Jurriaan Rot +1 more
View PDF Chat

Preservation of Equations by Monoidal Monads

2020-01-01
Louis Parlant , Jurriaan Rot , Alexandra Silva +1 more
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$ … 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\cdot y = y$) and relevant monads preserve dup equations (where some variable is duplicated, such as $x \cdot 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 the subclass of equations such that their preservation is equivalent to relevance.

A Categorical Framework for Learning Generalised Tree Automata

2022-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
View PDF Chat

Steps and Traces

2020-04-11
Jurriaan Rot , Bart Jacobs , Paul Blain 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 category. This paper … 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 category. This paper elaborates two new unifying ideas: 1) coalgebraic trace semantics is naturally presented in terms of corecursive algebras, and 2) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof, and allows to derive conditions under which some of them coincide.

Expressive Logics for Coinductive Predicates

2020-06-22
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 … 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.

Kleene Algebra with Observations

2018-11-16
Tobias Kappé , Paul Brunet , Jurriaan Rot +3 more
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms … Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

On Star Expressions and Coalgebraic Completeness Theorems.

2021-06-15
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. One … 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. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other.

Bisimilarity of open terms in stream GSOS

2018-11-12
Filippo Bonchi , Tom van Bussel , Matias David Lee +1 more
View PDF Chat

Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics

2019-08-22
Jorge A. Pérez , Jurriaan Rot
View PDF Chat

Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

2021-01-01
Yuichi Komorida , Shin-ya Katsumata , Clemens Kupke +2 more
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 (probabilistic, … 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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by K\"onig et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.
View PDF Chat

Learning Pomset Automata

2021-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +1 more
We extend the L* algorithm to learn bimonoids recognising pomset languages. We then identify a class of pomset automata that accepts precisely the class of pomset languages recognised by bimonoids … We extend the L* algorithm to learn bimonoids recognising pomset languages. We then identify a class of pomset automata that accepts precisely the class of pomset languages recognised by bimonoids and show how to convert between bimonoids and automata.
View PDF Chat

A Categorical Framework for Learning Generalised Tree Automata

2020-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
Automata learning is a popular technique used to automatically construct an automaton model from queries. Much research went into devising ad hoc adaptations of algorithms for different types of automata. … Automata learning is a popular technique used to automatically construct an automaton model from queries. Much research went into devising ad hoc adaptations of algorithms for different types of automata. The CALF project seeks to unify these using category theory in order to ease correctness proofs and guide the design of new algorithms. In this paper, we extend CALF to cover learning of algebraic structures that may not have a coalgebraic presentation. Furthermore, we provide a detailed algorithmic account of an abstract version of the popular L* algorithm, which was missing from CALF. We instantiate the abstract theory to a large class of Set functors, by which we recover for the first time practical tree automata learning algorithms from an abstract framework and at the same time obtain new algorithms to learn algebras of quotiented polynomial functors.
View PDF Chat

Coalgebraic Determinization of Alternating Automata

2018-01-01
Meven Bertrand , Jurriaan Rot
Coalgebra is a currently quite active field, which aims to look at generic state-based systems (most prominently automata) from a very abstract point of view, mainly using tools from category … Coalgebra is a currently quite active field, which aims to look at generic state-based systems (most prominently automata) from a very abstract point of view, mainly using tools from category theory. One of its achievements is to give a completely generic approach of determinization, unifying in an elegant manner non-deterministic automata, probabilistic automata or non-deterministic pushdown automata in one and the same model. However, the case of alternating automata fails to easily fit in this model. The aim of this internship was therefore to tackle this problem: can alternating automata also be determinized in the coalgebraic way? Does this give semantics that coincides with the concretely defined one? In this report, we give a positive answer to both questions. The main element of our construction is a distributive law, the definition of which has been for some time an open question.
View PDF Chat

Relational Connectors and Heterogeneous Bisimulations

2024-10-18
Pedro Nora , Jurriaan Rot , Lucas Deliga Schroder +1 more
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 relationships between systems of different … 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 relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances.
View PDF Chat

Bisimilarity of Open Terms in Stream GSOS

2017-01-01
Filippo Bonchi , Matias David Lee , Jurriaan Rot
View PDF Chat

Companions, Causality and Codensity

2017-01-01
Damien Pous , Jurriaan Rot
In the context of abstract coinduction in complete lattices, the notion of compatible function makes it possible to introduce enhancements of the coinduction proof principle. The largest compatible function, called … In the context of abstract coinduction in complete lattices, the notion of compatible function makes it possible to introduce enhancements of the coinduction proof principle. The largest compatible function, called the companion, subsumes most enhancements and has been proved to enjoy many good properties. Here we move to universal coalgebra, where the corresponding notion is that of a final distributive law. We show that when it exists, the final distributive law is a monad, and that it coincides with the codensity monad of the final sequence of the given functor. On sets, we moreover characterise this codensity monad using a new abstract notion of causality. In particular, we recover the fact that on streams, the functions definable by a distributive law or GSOS specification are precisely the causal functions. Going back to enhancements of the coinductive proof principle, we finally obtain that any causal function gives rise to a valid up-to-context technique.

Tree Automata as Algebras: Minimisation and Determinisation

2019-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
We study a categorical generalisation of tree automata, as $\Sigma$-algebras for a fixed endofunctor $\Sigma$ endowed with initial and final states. Under mild assumptions about the base category, we present … We study a categorical generalisation of tree automata, as $\Sigma$-algebras for a fixed endofunctor $\Sigma$ endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.
View PDF Chat

Fast Computations on Ordered Nominal Sets

2019-02-22
David Venhoek , Joshua Moerman , Jurriaan Rot
We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to … We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis. The approach is implemented as the library ONS (Ordered Nominal Sets). Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets. 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.

Coalgebra Learning via Duality

2019-02-15
Simone Barlocco , Clemens Kupke , Jurriaan Rot
Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. In this paper, we generalise learning to the theory of coalgebras. The approach relies on … Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. In this paper, we generalise learning to the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows us to learn, e.g., labelled transition systems, using Hennessy-Milner logic. Our main contribution is an abstract learning algorithm, together with a proof of correctness and termination.

Distributive laws for monotone specifications

2019-02-21
Jurriaan Rot
Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract … Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications-that disallow negative premises-do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation.
View PDF Chat

Learning Weighted Automata over Principal Ideal Domains

2019-11-11
Gerco van Heerdt , Clemens Kupke , Jurriaan Rot +1 more
In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal L* algorithm works when the semiring is a … In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal L* algorithm works when the semiring is a principal ideal domain, but not for general semirings such as the natural numbers.

Partially Observable Concurrent Kleene Algebra

2020-07-15
Jana Wagemaker , Paul Brunet , Simon Docherty +3 more
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that … We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.

Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

2021-05-21
Yuichi Komorida , Shin-ya Katsumata , Clemens Kupke +2 more
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 (probabilistic, … 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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by Konig et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.

Learning Automata with Name Allocation

2025-02-17
Florian Frank , Stefan Milius , Jurriaan Rot +1 more
Automata over infinite alphabets have emerged as a convenient computational model for processing structures involving data, such as nonces in cryptographic protocols or data values in XML documents. We introduce … Automata over infinite alphabets have emerged as a convenient computational model for processing structures involving data, such as nonces in cryptographic protocols or data values in XML documents. We introduce active learning methods for bar automata, a species of automata that process finite data words represented as bar strings, which are words with explicit name binding letters. Bar automata have pleasant algorithmic properties. We develop a framework in which every learning algorithm for standard deterministic or nondeterministic finite automata over finite alphabets can be used to learn bar automata, with a query complexity determined by that of the chosen learner. The technical key to our approach is the algorithmic handling of $\alpha$-equivalence of bar strings, which allows to bridge the gap between finite and infinite alphabets. The principles underlying our framework are generic and also apply to bar B\"uchi automata and bar tree automata, leading to the first active learning methods for data languages of infinite words and finite trees.
View PDF Chat

Correspondences between codensity and coupling-based liftings, a practical approach

2025-02-11
Samuel Humeau , Daniela Petrişan , 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 … 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.
View PDF Chat

Intrinsically Correct Sorting in Cubical Agda

2025-01-10
Cass Alexandru , Vikraman Choudhury , Jurriaan Rot +1 more
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 functors they construct pairs … 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 functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.
View PDF Chat

Relational Connectors and Heterogeneous Simulations

2025-01-01
Pedro Nora , Jurriaan Rot , Lutz Schröder +1 more

Complete Test Suites for Automata in Monoidal Closed Categories

2025-01-01
Bálint Kocsis , Jurriaan Rot

Complete Test Suites for Automata in Monoidal Closed Categories

2024-11-20
Béla Kocsis , Jurriaan Rot
Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, … Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the specification. We introduce a framework for proving completeness of test suites at the general level of automata in monoidal closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for weighted automata and deterministic nominal automata.
View PDF Chat

Relational Connectors and Heterogeneous Bisimulations

2024-10-18
Pedro Nora , Jurriaan Rot , Lucas Deliga Schroder +1 more
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 relationships between systems of different … 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 relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances.
View PDF Chat

A Unifying Approach to Product Constructions for Quantitative Temporal Inference

2024-07-15
Kazuki Watanabe , Sebastian Junges , Jurriaan Rot +1 more
Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temporal inference: to compute the likelihood that the … Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temporal inference: to compute the likelihood that the execution traces satisfy a given temporal property. This paper presents a general framework for temporal inference, which applies to a rich variety of quantitative models including those that arise in the operational semantics of probabilistic and weighted programs. The key idea underlying our framework is that in a variety of existing approaches, the main construction that enables temporal inference is that of a product between the system of interest and the temporal property. We provide a unifying mathematical definition of product constructions, enabled by the realisation that 1) both systems and temporal properties can be modelled as coalgebras and 2) product constructions are distributive laws in this context. Our categorical framework leads us to our main contribution: a sufficient condition for correctness, which is precisely what enables to use the product construction for temporal inference. We show that our framework can be instantiated to naturally recover a number of disparate approaches from the literature including, e.g., partial expected rewards in Markov reward models, resource-sensitive reachability analysis, and weighted optimization problems. Further, we demonstrate a product of weighted programs and weighted temporal properties as a new instance to show the scalability of our approach.
View PDF Chat

State Matching and Multiple References in Adaptive Active Automata Learning

2024-06-28
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 domain specific … 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 domain specific knowledge in the form of (similar) reference models. Such reference models appear naturally when learning multiple versions or variants of a software system. In this paper, we present state matching, which allows flexible use of the structure of these reference models by the learner. State matching is the main ingredient of adaptive L#, a novel framework for adaptive learning, built on top of L#. Our empirical evaluation shows that adaptive L# improves the state of the art by up to two orders of magnitude.
View PDF Chat

Composing Codensity Bisimulations

2024-06-21
Mayuko Kori , Kazuki Watanabe , Jurriaan Rot +1 more
View PDF Chat

On Tools for Completeness of Kleene Algebra with Hypotheses

2024-05-16
Damien Pous , Jurriaan Rot , Jana Wagemaker
In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the … In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.
View PDF Chat

A Categorical Approach to Coalgebraic Fixpoint Logic

2024-04-30
Ezra Schoen , Clemens Kupke , Jurriaan Rot +1 more
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 categories. We give a least-solution semantics as … 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 categories. We give a least-solution semantics as well as an initial algebra semantics, and prove they are equivalent. We also show how to place the alternation-free coalgebraic $\mu$-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality.
View PDF Chat

Proving Behavioural Apartness

2024-04-25
Ruben Turkenburg , Harsh Beohar , Clemens Kupke +1 more
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 yields the possibility of … 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 yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems. We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples.
View PDF Chat

Composing Codensity Bisimulations

2024-04-12
Mayuko Kori , Kazuki Watanabe , Jurriaan Rot +1 more
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 formulation of this problem, where operations … 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 formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system. In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality. ...
View PDF Chat

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

2024-01-01
Kazuki Watanabe , Marck van der Vegt , Ichiro Hasuo +2 more
Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. … Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers string diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a Pareto curve on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach.
View PDF Chat

Small Test Suites for Active Automata Learning

2024-01-01
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 counterexamples is given by … 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 counterexamples is given by so-called test suites, consisting of input sequences that have to be checked to decide whether a counterexample exists. This paper shows that significantly smaller test suites suffice under reasonable assumptions on the structure of the black box. These smaller test suites help to refute false hypotheses during active automata learning, even when the assumptions do not hold. We combine multiple test suites using a multi-armed bandit setup that adaptively selects a test suite. An extensive empirical evaluation shows the efficacy of our approach. For small to medium-sized models, the performance gain is limited. However, the approach allows learning models from large, industrial case studies that were beyond the reach of known methods.
View PDF Chat

Relating Apartness and Branching Bisimulation Games

2024-01-01
Jurriaan Rot , Sebastian Junges , Harsh Beohar
View PDF Chat

Bisimilar States in Uncertain Structures

2023-01-01
Jurriaan Rot , Thorsten Wißmann
We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in … We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in automata learning algorithms, where one investigates whether two observed behaviours come from the same internal state of a black-box system that can not be transparently inspected. We model this uncertainty as a set functor equipped with a partial order which describes possible future developments of the learning game. On such a functor, we provide a lifting-based definition of uncertain bisimilarity and verify basic properties. Beside its applications to Mealy machines, a natural model for automata learning, our framework also instantiates to an existing compatibility relation on suspension automata, which are used in model-based testing. We show that uncertain bisimilarity is a necessary but not sufficient condition for two states being implementable by the same state in the black-box system. To remedy the failure of the one direction, we characterize uncertain bisimilarity in terms of coalgebraic simulations.

Fast computations on ordered nominal sets

2022-09-06
David Venhoek , Joshua Moerman , Jurriaan Rot
View PDF Chat

A Categorical Framework for Learning Generalised Tree Automata

2022-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
View PDF Chat

Processes Parametrised by an Algebraic Theory

2022-01-01
Todd Schmid , Wojciech Różowski , Alexandra Silva +1 more
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 process terms and a … 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 process terms and a complete axiomatisation of semantic equivalence. We show that there are uniformly defined fragments of our calculi that capture well-known examples from the literature like regular expressions modulo bisimilarity and guarded Kleene algebra with tests. We also derive new calculi for probabilistic and convex processes with an analogue of Kleene star.

Concurrent NetKAT

2022-01-01
Jana Wagemaker , Nate Foster , Tobias Kappé +3 more
We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. We provide a model of … We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. We provide a model of the language based on partially-ordered multisets (pomsets), which are a well-established mathematical structure for defining the denotational semantics of concurrent languages. We provide a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through examples. More generally, CNetKAT can be understood as an algebraic framework for reasoning about programs with both local state (in packets) and global state (in a global store).
View PDF Chat

On Tools for Completeness of Kleene Algebra with Hypotheses

2022-01-01
Damien Pous , Jurriaan Rot , Jana Wagemaker
In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the … In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.
View PDF Chat

On Star Expressions and Completeness Theorems

2021-12-27
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. One … 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. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other.
View PDF Chat

Expressive Logics for Coinductive Predicates

2021-12-15
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 … 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.
View PDF Chat

Steps and traces

2021-07-14
Jurriaan Rot , Bart Jacobs , Paul Blain Levy
Abstract 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 category. This … Abstract 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 category. This paper elaborates two new unifying ideas: (i) coalgebraic,draftrules trace semantics is naturally presented in terms of corecursive algebras, and (ii) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof and allows to derive conditions under which some of them coincide.
View PDF Chat

Expressivity of Quantitative Modal Logics : Categorical Foundations via Codensity and Approximation

2021-06-29
Yuichi Komorida , Shin-ya Katsumata , Clemens Kupke +2 more
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 (probabilistic, … 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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting-a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by König et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.
View PDF Chat

On Star Expressions and Coalgebraic Completeness Theorems.

2021-06-15
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. One … 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. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other.

Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

2021-05-21
Yuichi Komorida , Shin-ya Katsumata , Clemens Kupke +2 more
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 (probabilistic, … 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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by Konig et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.

Learning Pomset Automata

2021-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +1 more
View PDF Chat

A New Approach for Active Automata Learning Based on Apartness

2021-01-01
Frits Vaandrager , Bharat Garhewal , Jurriaan Rot +1 more
We present $L^{\#}$, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $L^{\ast}$ algorithm and its descendants, $L^{\#}$ takes a different … We present $L^{\#}$, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $L^{\ast}$ algorithm and its descendants, $L^{\#}$ takes a different perspective: it tries to establish apartness, a constructive form of inequality. $L^{\#}$ does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. $L^{\#}$ has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of $L^{\#}$ in practice. Experiments with a prototype implementation, written in Rust, suggest that $L^{\#}$ is competitive with existing algorithms.

Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

2021-01-01
Yuichi Komorida , Shin-ya Katsumata , Clemens Kupke +2 more
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 (probabilistic, … 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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by K\"onig et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.
View PDF Chat

Learning Pomset Automata

2021-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +1 more
We extend the L* algorithm to learn bimonoids recognising pomset languages. We then identify a class of pomset automata that accepts precisely the class of pomset languages recognised by bimonoids … We extend the L* algorithm to learn bimonoids recognising pomset languages. We then identify a class of pomset automata that accepts precisely the class of pomset languages recognised by bimonoids and show how to convert between bimonoids and automata.
View PDF Chat

Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics

2020-08-27
Ornela Dardha , Jurriaan Rot
View PDF Chat

Partially Observable Concurrent Kleene Algebra

2020-07-15
Jana Wagemaker , Paul Brunet , Simon Docherty +3 more
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that … We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.

Expressive Logics for Coinductive Predicates

2020-06-22
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 … 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.

Steps and Traces

2020-04-11
Jurriaan Rot , Bart Jacobs , Paul Blain 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 category. This paper … 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 category. This paper elaborates two new unifying ideas: 1) coalgebraic trace semantics is naturally presented in terms of corecursive algebras, and 2) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof, and allows to derive conditions under which some of them coincide.

Preservation of Equations by Monoidal Monads

2020-01-01
Louis Parlant , Jurriaan Rot , Alexandra Silva +1 more
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$ … 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\cdot y = y$) and relevant monads preserve dup equations (where some variable is duplicated, such as $x \cdot 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 the subclass of equations such that their preservation is equivalent to relevance.

Preservation of Equations by Monoidal Monads

2020-01-01
Louis Parlant , Jurriaan Rot , Alexandra Silva +1 more
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 … 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.

Partially Observable Concurrent Kleene Algebra

2020-01-01
Jana Wagemaker , Paul Brunet , Simon Docherty +3 more
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that … We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.
View PDF Chat

Up-to Techniques for Branching Bisimilarity

2020-01-01
Rick Erkens , Jurriaan Rot , Bas Luttik
View PDF Chat

A Categorical Framework for Learning Generalised Tree Automata

2020-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
Automata learning is a popular technique used to automatically construct an automaton model from queries. Much research went into devising ad hoc adaptations of algorithms for different types of automata. … Automata learning is a popular technique used to automatically construct an automaton model from queries. Much research went into devising ad hoc adaptations of algorithms for different types of automata. The CALF project seeks to unify these using category theory in order to ease correctness proofs and guide the design of new algorithms. In this paper, we extend CALF to cover learning of algebraic structures that may not have a coalgebraic presentation. Furthermore, we provide a detailed algorithmic account of an abstract version of the popular L* algorithm, which was missing from CALF. We instantiate the abstract theory to a large class of Set functors, by which we recover for the first time practical tree automata learning algorithms from an abstract framework and at the same time obtain new algorithms to learn algebras of quotiented polynomial functors.
View PDF Chat

Steps and Traces

2020-01-01
Jurriaan Rot , Bart Jacobs , Paul Blain 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 category. This paper … 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 category. This paper elaborates two new unifying ideas: 1) coalgebraic trace semantics is naturally presented in terms of corecursive algebras, and 2) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof, and allows to derive conditions under which some of them coincide.

Learning Weighted Automata over Principal Ideal Domains

2019-11-11
Gerco van Heerdt , Clemens Kupke , Jurriaan Rot +1 more
In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal L* algorithm works when the semiring is a … In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal L* algorithm works when the semiring is a principal ideal domain, but not for general semirings such as the natural numbers.

Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics

2019-08-22
Jorge A. Pérez , Jurriaan Rot
View PDF Chat

Separation and Renaming in Nominal Sets

2019-06-03
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 … 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. These automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Fast Computations on Ordered Nominal Sets

2019-02-22
David Venhoek , Joshua Moerman , Jurriaan Rot
We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to … We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis. The approach is implemented as the library ONS (Ordered Nominal Sets). Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets. 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.

Distributive laws for monotone specifications

2019-02-21
Jurriaan Rot
Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract … Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications-that disallow negative premises-do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation.
View PDF Chat

Coalgebra Learning via Duality

2019-02-15
Simone Barlocco , Clemens Kupke , Jurriaan Rot
Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. In this paper, we generalise learning to the theory of coalgebras. The approach relies on … Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. In this paper, we generalise learning to the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows us to learn, e.g., labelled transition systems, using Hennessy-Milner logic. Our main contribution is an abstract learning algorithm, together with a proof of correctness and termination.

Tree Automata as Algebras: Minimisation and Determinisation

2019-01-01
Gerco van Heerdt , Tobias Kappé , Jurriaan Rot +2 more
We study a categorical generalisation of tree automata, as $\Sigma$-algebras for a fixed endofunctor $\Sigma$ endowed with initial and final states. Under mild assumptions about the base category, we present … We study a categorical generalisation of tree automata, as $\Sigma$-algebras for a fixed endofunctor $\Sigma$ endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.
View PDF Chat
Coauthor Papers Together
Alexandra Silva 19
Tobias Kappé 12
Clemens Kupke 11
Gerco van Heerdt 8
Jana Wagemaker 8
Marcello Bonsangue 6
Joshua Moerman 5
Sebastian Junges 5
Ichiro Hasuo 5
Damien Pous 5
Shin-ya Katsumata 5
Matteo Sammartino 4
Paul Brunet 4
Paul Blain Levy 4
Todd Schmid 3
Yuichi Komorida 3
David Venhoek 3
Bart Jacobs 3
Filippo Bonchi 3
Helle Hvid Hansen 2
Ruben Turkenburg 2
P. Wild 2
Thorsten Wißmann 2
Bas Westerbaan 2
Mayuko Kori 2
Stefan Milius 2
Fabio Zanasi 2
Simon Docherty 2
Loes Kruger 2
Louis Parlant 2
Kazuki Watanabe 2
Kazuki Watanabe 2
Meven Bertrand 2
Pedro Nora 2
Matias David Lee 2
Simone Barlocco 2
Alexander Kurz 2
Rick Erkens 1
Henning Basold 1
Nate Foster 1
Tom van Bussel 1
Wojciech Różowski 1
Bharat Garhewal 1
Bartek Klin 1
Ezra Schoen 1
Jorge A. Pérez 1
Béla Kocsis 1
Julian Salamanca 1
Daniela Petrişan 1
Henning Urbat 1

Coalgebraic Modal Logic Beyond Sets

2007-04-01
Bartek Klin
Polyadic coalgebraic modal logic is studied in the setting of locally presentable categories. It is shown that under certain assumptions, accessible functors admit expressive logics for their coalgebras. Examples include … Polyadic coalgebraic modal logic is studied in the setting of locally presentable categories. It is shown that under certain assumptions, accessible functors admit expressive logics for their coalgebras. Examples include typical functors used to describe systems with name binding, interpreted in nominal sets.
View PDF Chat

Adjoint Lifting Theorems for Categories of Algebras

1975-11-01
Peter Johnstone

Learning nominal automata

2016-12-22
Joshua Moerman , Matteo Sammartino , Alexandra Silva +2 more
We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations … We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations of the algorithm to this new setting. In particular we can learn a subclass of nominal non-deterministic automata. An implementation using a recently developed Haskell library for nominal computation is provided for preliminary experiments.
View PDF Chat

Simulations in coalgebra

2004-08-10
Jesse Hughes , Bart Jacobs
View PDF Chat

Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads

2000-01-01
Marina Lenisa , John Power , Hiroshi Watanabe
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate Eilenberg-Moore and … We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate Eilenberg-Moore and Kleisli constructions for each of these possibilities. Then we consider two applications of these weakened notions of distributivity in detail. We characterise Turi and Plotkin's model of GSOS as a distributive law of a monad over a co-pointed endofunctor, and we analyse generalised coiteration and coalgebraic coinduction "up-to" in terms of a distributive law of the underlying pointed endofunctor of a monad over an endofunctor.

Generalizing determinization from automata to coalgebras

2013-03-04
Alexandra Silva , Filippo Bonchi , Marcello Bonsangue +1 more
The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata … The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics.
View PDF Chat

Coalgebraic trace semantics via forgetful logics

2017-04-27
Bartek Klin , Jurriaan Rot
We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and … We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition under which a logical semantics coincides with the trace semantics obtained via a given determinization construction. Finally, we consider a condition that guarantees the existence of a canonical determinization procedure that is correct with respect to a given logical semantics. That procedure is closely related to Brzozowski's minimization algorithm.
View PDF Chat

Generic Trace Semantics via Coinduction

2007-11-19
Ichiro Hasuo , Bart Jacobs , Ana Sokolova
Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs. probability. In this paper we claim to identify one … Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs. probability. In this paper we claim to identify one underlying mathematical structure behind these "trace semantics," namely coinduction in a Kleisli category. This claim is based on our technical result that, under a suitably order-enriched setting, a final coalgebra in a Kleisli category is given by an initial algebra in the category Sets. Formerly the theory of coalgebras has been employed mostly in Sets where coinduction yields a finer process semantics of bisimilarity. Therefore this paper extends the application field of coalgebras, providing a new instance of the principle "process semantics via coinduction."
View PDF Chat

Automata theory in nominal sets

2014-08-15
Mikołaj Bojańczyk , Bartek Klin , Sławomir Lasota
We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, … We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.
View PDF Chat

Codensity Games for Bisimilarity

2019-06-01
Yuichi Komorida , Shin-ya Katsumata , Nick Hu +2 more
Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been … Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including what we call bisimulation topology).
View PDF Chat

Categories for the Working Mathematician

1971-01-01
Saunders Mac Lane
View PDF Chat

Simplified Coalgebraic Trace Equivalence

2015-01-01
Alexander Kurz , Stefan Milius , Dirk Pattinson +1 more
View PDF Chat

A van Benthem Theorem for Fuzzy Modal Logic

2018-06-27
P. Wild , Lutz Schröder , Dirk Pattinson +1 more
We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy … We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with its modal fragment, and show that the fuzzy first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exactly those that can be approximated by fuzzy modal formulas.
View PDF Chat

Concurrent Kleene Algebra: Free Model and Completeness

2018-01-01
Tobias Kappé , Paul Brunet , Alexandra Silva +1 more
Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the axioms for CKA with … Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the axioms for CKA with bounded parallelism are complete for the semantics proposed in the original paper; consequently, these semantics are the free model for this fragment. This result settles a conjecture of Hoare and collaborators. Moreover, the technique developed to this end allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.
View PDF Chat

Iterated Covariant Powerset is not a Monad

2018-12-01
Bartek Klin , Julian Salamanca
We prove that the double covariant powerset functor PP does not admit any monad structure. The same applies to the n-fold composition of P for any n>1. We prove that the double covariant powerset functor PP does not admit any monad structure. The same applies to the n-fold composition of P for any n>1.

The formal theory of monads II

2002-11-01
Stephen Lack , Ross Street

Sound and Complete Axiomatizations of Coalgebraic Language Equivalence

2013-02-01
Marcello Bonsangue , Stefan Milius , Alexandra Silva
Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use of the coalgebraic view on systems to investigate, in a … Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalised powerset construction that determinises coalgebras. We show that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the given type functor. Our main result is that the rational fixpoint of the functor $FT$, where $T$ is a monad describing the branching of the systems (e.g. non-determinism, weights, probability etc.), has as a quotient the rational fixpoint of the "determinised" type functor $\bar F$, a lifting of $F$ to the category of $T$-algebras. We apply our framework to the concrete example of weighted automata, for which we present a new sound and complete calculus for weighted language equivalence. As a special case, we obtain non-deterministic automata, where we recover Rabinovich's sound and complete calculus for language equivalence.
View PDF Chat

Bisimilarity in Fresh-Register Automata

2015-07-01
Andrzej S. Murawski , Steven J. Ramsay , Nikos Tzevelekos
Register automata are a basic model of computation over infinite alphabets.Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name … Register automata are a basic model of computation over infinite alphabets.Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation.This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata.We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty.In the general case, we show that the problem is EXPTIME-complete.However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies.Furthermore, they enable a highly succinct representation of the corresponding bisimulations.By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines.In each case, we find that freshness does not affect the complexity class of the problem.The results allow us to close a complexity gap for language equivalence of deterministic register automata.We show that deterministic language inequivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto.Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.
View PDF Chat

Expressive Logics for Coinductive Predicates

2021-12-15
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 … 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.
View PDF Chat

Learning Automata with Side-Effects

2017-04-26
Gerco van Heerdt , Matteo Sammartino , Alexandra Silva
Automata learning has been successfully applied in the verification of hardware and software. The size of the automaton model learned is a bottleneck for scalability and hence optimizations that enable … Automata learning has been successfully applied in the verification of hardware and software. The size of the automaton model learned is a bottleneck for scalability and hence optimizations that enable learning of compact representations are important. In this paper, we continue the development of a general framework for automata learning based on category theory and develop a class of optimizations and an accompanying correctness proof for learning algorithms. The new algorithm is parametric on a monad, which provides a rich algebraic structure to capture non-determinism and other side-effects. These side-effects are used to learn more compact automaton models and the abstract categorical approach enables us to capture several possible optimizations under the same (p)roof.

Coalgebra-to-Algebra Morphisms

1999-01-01
A. Eppendahl
Given a coalgebra p for HG, an algebra s for GH and the obvious notion of morphism from coalgebra to algebra, we observe that morphisms from Gp to s correspond … Given a coalgebra p for HG, an algebra s for GH and the obvious notion of morphism from coalgebra to algebra, we observe that morphisms from Gp to s correspond to morphisms from p to Hs in the manner of an adjunction even when there is no adjunction between G and H. This appears to be one of the basic phenomena underlying the transport of special algebras. A proof of Freyd's Iterated Square Theorem illustrates the interaction with Lambek's Lemma.

A Coalgebraic Approach to Quantitative Linear Time Logics.

2016-12-23
Corina Cı̂rstea
We define quantitative fixpoint logics for reasoning about linear time properties of states in systems with branching behaviour. We model such systems as coalgebras whose type arises as the composition … We define quantitative fixpoint logics for reasoning about linear time properties of states in systems with branching behaviour. We model such systems as coalgebras whose type arises as the composition of a branching monad with one or more polynomial endofunctors on the category of sets. The domain of truth values for our logics is determined by the choice of branching monad, as is the special modality used to abstract away branching in the semantics of the logics. To justify our choice of syntax and semantics for the logics, we prove the equivalence between their step-wise semantics and an alternative path-based semantics for the fixpoint-free fragments of the logics. Instances of these logics support reasoning about the possibility, probability or minimal cost of exhibiting a given linear time property. We conclude with two examples of logics that have a linear time flavour but do not admit a path-based semantics, namely a logic for reasoning about resource usage in infinitely-running computations, and a quantitative logic for reasoning about component interaction.

Coalgebraic Behavioral Metrics

2017-01-01
Paolo Baldan , Filippo Bonchi , Henning Kerstan +1 more
We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $\alpha\colon X \to HX$ for a functor $H … We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $\alpha\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a functor $\overline{H}$ on the category $\mathrm{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. If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model linear-time metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction.
View PDF Chat

Lax extensions of coalgebra functors and their logic

2014-12-05
Johannes Marti , Yde Venema

Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time

2019-12-20
Steffen Smolka , Nate Foster , Justin Hsu +3 more
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded … Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra.
View PDF Chat

Simulations and Bisimulations for Coalgebraic Modal Logics

2013-01-01
Daniel Gorín , Lutz Schröder
View PDF Chat

Simulations in Coalgebra

2003-07-01
Bart Jacobs , Jesse Hughes
A new approach to simulations is proposed within the theory of coalgebras by taking a notion of order on a functor as primitive. Such an order forms a basic building … A new approach to simulations is proposed within the theory of coalgebras by taking a notion of order on a functor as primitive. Such an order forms a basic building block for a “lax relation lifting”, or “relator” as used by other authors. Simulations appear as coalgebras of this lifted functor, and similarity as greatest simulation. Two-way similarity is then similarity in both directions. In general, it is different from bisimilarity (in the usual coalgebraic sense), but a sufficient condition is formulated (and illustrated) to ensure that bisimilarity and two-way similarity coincide. Also, a distributive law is identified which ensures that similarity on a final coalgebra forms a dcpo structure.

Modern Applied Algebra.

1972-05-01
Eugene A. Klotz , Garrett Birkhoff , Thomas C. Bartee

Completely iterative algebras and completely iterative monads

2004-12-13
Stefan Milius

Kan extensions in Enriched Category Theory

1970-01-01
Eduardo J. Dubuc
View PDF Chat

Programming interfaces and basic topology

2005-06-24
Peter Hancock , Pierre Hyvernat
View PDF Chat

Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness

2020-01-01
Tobias Kappé , Paul Brunet , Alexandra Silva +2 more
View PDF Chat

Kleene Algebra with Tests and Coq Tools for while Programs

2013-01-01
Damien Pous
View PDF Chat

An Efficient Coq Tactic for Deciding Kleene Algebras

2010-01-01
Thomas Braibant , Damien Pous
View PDF Chat

On approximation theorems for uniform spaces

1971-03-01
Á. Császár

A complete system of B-rational identities

2005-12-11
Daniel Krob

Equational presentations of functors and monads

2011-03-25
Jiřı́ Velebil , Alexander Kurz
We study equational presentations of functors and monads defined on a category that is equipped by an adjunction F ˧ U : → of descent type. We present a class … We study equational presentations of functors and monads defined on a category that is equipped by an adjunction F ˧ U : → of descent type. We present a class of functors/monads that admit such an equational presentation that involves finitary signatures in . We apply these results to an equational description of functors arising in various areas of theoretical computer science.

Terminal coalgebras in well-founded set theory

1993-06-01
Michael Barr

A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on

1980-08-01
G. M. Kelly
Many problems lead to the consideration of “algebras”, given by an object A of a category A together with “actions” T k A → A on A of one or … Many problems lead to the consideration of “algebras”, given by an object A of a category A together with “actions” T k A → A on A of one or more endofunctors of A, subjected to equational axioms. Such problems include those of free monads and free monoids, of cocompleteness in categories of monads and of monoids, of orthogonal subcategories (= generalized sheaf-categories), of categories of continuous functors, and so on; apart from problems involving the algebras for their own sake. Desirable properties of the category of algebras - existence of free ones, cocompleteness, existence of adjoints to algebraic functors - all follow if this category can be proved reflective in some well-behaved category: for which we choose a certain comma-category T/A We show that the reflexion exists and is given as the colimit of a simple transfinite sequence, if A is cocomplete and the T k preserve either colimits or unions of suitably-long chains of subobjects. The article draws heavily on the work of earlier authors, unifies and simplifies this, and extends it to new problems. Moreover the reflectivity in T/A is stronger than any earlier result, and will be applied in forthcoming articles, in an enriched version, to the study of categories with structure.
View PDF Chat

The Power of Convex Algebras

2017-07-07
Filippo Bonchi , Alexandra Silva , Ana Sokolova
Probabilistic automata (PA) combine probability and nondeterminism. They can be given different semantics, like strong bisimilarity, convex bisimilarity, or (more recently) distribution bisimilarity. The latter is based on the view … Probabilistic automata (PA) combine probability and nondeterminism. They can be given different semantics, like strong bisimilarity, convex bisimilarity, or (more recently) distribution bisimilarity. The latter is based on the view of PA as transformers of probability distributions, also called belief states, and promotes distributions to first-class citizens. We give a coalgebraic account of the latter semantics, and explain the genesis of the belief-state transformer from a PA. To do so, we make explicit the convex algebraic structure present in PA and identify belief-state transformers as transition systems with state space that carries a convex algebra. As a consequence of our abstract approach, we can give a sound proof technique which we call bisimulation up-to convex hull.

Fast Computations on Ordered Nominal Sets

2018-01-01
David Venhoek , Joshua Moerman , Jurriaan Rot
View PDF Chat

(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras

2017-01-01
Barbara König , Christina Mika-Michalski
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 … 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.

Relators and Metric Bisimulations

1998-01-01
J.J.M.M. Rutten
Coalgebras of set functors preserving weak pullbacks are particularly well-behaved. Invoking a result by Carboni, Kelly, and Wood (1990), we show that this can be explained by the fact that … Coalgebras of set functors preserving weak pullbacks are particularly well-behaved. Invoking a result by Carboni, Kelly, and Wood (1990), we show that this can be explained by the fact that such functors can be uniquely extended to a relator. This insight next suggests a definition of metric bisimulation.

History-Register Automata

2016-03-29
Radu Grigore , Nikos Tzevelekos
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic … Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
View PDF Chat

Lifting theorems for Kleisli categories

1994-01-01
Philip S. Mulry

An Invitation to C*-Algebras

1976-01-01
William Arveson

SMT Solving for Functional Programming over Infinite Structures

2016-04-01
Bartek Klin , Michał Szynwelski
We develop a simple functional programming language aimed at manipulating infinite, but first-order definable structures, such as the countably infinite clique graph or the set of all intervals with rational … We develop a simple functional programming language aimed at manipulating infinite, but first-order definable structures, such as the countably infinite clique graph or the set of all intervals with rational endpoints. Internally, such sets are represented by logical formulas that define them, and an external satisfiability modulo theories (SMT) solver is regularly run by the interpreter to check their basic properties. The language is implemented as a Haskell module.
View PDF Chat

On tree coalgebras and coalgebra presentations

2003-08-01
Jiřı́ Adámek , Hans-E. Porst

Homomorphisms of Coalgebras from Predicate Liftings

2013-01-01
Sebastian Enqvist

Une remarque sur les systèmes complets d'identités rationnelles

1990-01-01
Maurice Boffa
Une regle deductive tres simple permet de relier des problemes de completude souleves par Conway et Salomaa Une regle deductive tres simple permet de relier des problemes de completude souleves par Conway et Salomaa
View PDF Chat