Showing 1–43 of 43 results for author: Rot, J

State Matching and Multiple References in Adaptive Active Automata Learning

Authors: Loes Kruger, Sebastian Junges, Jurriaan Rot

Abstract: 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, whic… ▽ More 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. △ Less

Submitted 28 June, 2024; originally announced June 2024.

Comments: Extended paper for FM 2024

Scorch: A Library for Sparse Deep Learning

Authors: Bobby Yan, Alexander J. Root, Trevor Gale, David Broman, Fredrik Kjolstad

Abstract: The rapid growth in the size of deep learning models strains the capabilities of traditional dense computation paradigms. Leveraging sparse computation has become increasingly popular for training and deploying large-scale models, but existing deep learning frameworks lack extensive support for sparse operations. To bridge this gap, we introduce Scorch, a library that seamlessly integrates efficie… ▽ More The rapid growth in the size of deep learning models strains the capabilities of traditional dense computation paradigms. Leveraging sparse computation has become increasingly popular for training and deploying large-scale models, but existing deep learning frameworks lack extensive support for sparse operations. To bridge this gap, we introduce Scorch, a library that seamlessly integrates efficient sparse tensor computation into the PyTorch ecosystem, with an initial focus on inference workloads on CPUs. Scorch provides a flexible and intuitive interface for sparse tensors, supporting diverse sparse data structures. Scorch introduces a compiler stack that automates key optimizations, including automatic loop ordering, tiling, and format inference. Combined with a runtime that adapts its execution to both dense and sparse data, Scorch delivers substantial speedups over hand-written PyTorch Sparse (torch.sparse) operations without sacrificing usability. More importantly, Scorch enables efficient computation of complex sparse operations that lack hand-optimized PyTorch implementations. This flexibility is crucial for exploring novel sparse architectures. We demonstrate Scorch's ease of use and performance gains on diverse deep learning models across multiple domains. With only minimal code changes, Scorch achieves 1.05-5.78x speedups over PyTorch Sparse on end-to-end tasks. Scorch's seamless integration and performance gains make it a valuable addition to the PyTorch ecosystem. We believe Scorch will enable wider exploration of sparsity as a tool for scaling deep learning and inform the development of other sparse libraries. △ Less

Submitted 20 June, 2024; v1 submitted 27 May, 2024; originally announced May 2024.

Comments: 25 pages, 8 figures

A Categorical Approach to Coalgebraic Fixpoint Logic

Authors: Ezra Schoen, Clemens Kupke, Jurriaan Rot, Ruben Turkenburg

Abstract: 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 $μ$-calculus in this framework, as well as PDL a… ▽ 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 well as an initial algebra semantics, and prove they are equivalent. We also show how to place the alternation-free coalgebraic $μ$-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality. △ Less

Submitted 30 April, 2024; originally announced May 2024.

Proving Behavioural Apartness

Authors: Ruben Turkenburg, Harsh Beohar, Clemens Kupke, Jurriaan Rot

Abstract: 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 motivat… ▽ 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 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. △ Less

Submitted 25 April, 2024; originally announced April 2024.

Composing Codensity Bisimulations

Authors: Mayuko Kori, Kazuki Watanabe, Jurriaan Rot, Shin-ya Katsumata

Abstract: 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… ▽ 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 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. ... △ Less

Submitted 21 May, 2024; v1 submitted 12 April, 2024; originally announced April 2024.

Comments: Extended version (includes the Appendix) of the paper accepted at LiCS-24

MSC Class: 68Q85

Stable matching as transportation

Authors: Federico Echenique, Joseph Root, Fedor Sandomirskiy

Abstract: We study matching markets with aligned preferences and establish a connection between common design objectives -- stability, efficiency, and fairness -- and the theory of optimal transport. Optimal transport gives new insights into the structural properties of matchings obtained from pursuing these objectives, and into the trade-offs between different objectives. Matching markets with aligned pref… ▽ More We study matching markets with aligned preferences and establish a connection between common design objectives -- stability, efficiency, and fairness -- and the theory of optimal transport. Optimal transport gives new insights into the structural properties of matchings obtained from pursuing these objectives, and into the trade-offs between different objectives. Matching markets with aligned preferences provide a tractable stylized model capturing supply-demand imbalances in a range of settings such as partnership formation, school choice, organ donor exchange, and markets with transferable utility where bargaining over transfers happens after a match is formed. △ Less

Submitted 20 February, 2024; originally announced February 2024.

MSC Class: 91B68; 90C08

Small Test Suites for Active Automata Learning

Authors: Loes Kruger, Sebastian Junges, Jurriaan Rot

Abstract: 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 reasonabl… ▽ More 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. △ Less

Submitted 23 January, 2024; originally announced January 2024.

Comments: Extended paper for TACAS 2024

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

Authors: Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, Sebastian Junges

Abstract: 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 challen… ▽ 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. 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. △ Less

Submitted 16 January, 2024; originally announced January 2024.

Comments: Extended version (includes the Appendix) of the paper accepted at TACAS-24

Bisimilar States in Uncertain Structures

Authors: Jurriaan Rot, Thorsten Wißmann

Abstract: 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… ▽ More 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. △ Less

Submitted 27 March, 2023; originally announced March 2023.

On Tools for Completeness of Kleene Algebra with Hypotheses

Authors: Damien Pous, Jurriaan Rot, Jana Wagemaker

Abstract: 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… ▽ More 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. △ Less

Submitted 15 May, 2024; v1 submitted 24 October, 2022; originally announced October 2022.

Efficiency in Random Resource Allocation and Social Choice

Authors: Federico Echenique, Joseph Root, Fedor Sandomirskiy

Abstract: We study efficiency in general collective choice problems where agents have ordinal preferences and randomization is allowed. We explore the structure of preference profiles where ex-ante and ex-post efficiency coincide, offer a unifying perspective on the known results, and give several new characterizations. The results have implications for well-studied mechanisms including random serial dictat… ▽ More We study efficiency in general collective choice problems where agents have ordinal preferences and randomization is allowed. We explore the structure of preference profiles where ex-ante and ex-post efficiency coincide, offer a unifying perspective on the known results, and give several new characterizations. The results have implications for well-studied mechanisms including random serial dictatorship and a number of specific environments, including the dichotomous, single-peaked, and social choice domains. △ Less

Submitted 19 August, 2022; v1 submitted 12 March, 2022; originally announced March 2022.

Processes Parametrised by an Algebraic Theory

Authors: Todd Schmid, Wojciech Rozowski, Alexandra Silva, Jurriaan Rot

Abstract: 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 b… ▽ 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 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. △ Less

Submitted 25 July, 2022; v1 submitted 14 February, 2022; originally announced February 2022.

Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks

Authors: Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, Alexandra Silva

Abstract: 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… ▽ 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 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). △ Less

Submitted 12 July, 2022; v1 submitted 25 January, 2022; originally announced January 2022.

Journal ref: Proc. ESOP 2022, pp 575-602

A New Approach for Active Automata Learning Based on Apartness

Authors: Frits Vaandrager, Bharat Garhewal, Jurriaan Rot, Thorsten Wißmann

Abstract: 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 dire… ▽ 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 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. △ Less

Submitted 27 January, 2022; v1 submitted 12 July, 2021; originally announced July 2021.

On Star Expressions and Coalgebraic Completeness Theorems

Authors: Todd Schmid, Jurriaan Rot, Alexandra Silva

Abstract: 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… ▽ More 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. △ Less

Submitted 8 March, 2022; v1 submitted 15 June, 2021; originally announced June 2021.

Comments: In Proceedings MFPS 2021, arXiv:2112.13746

Journal ref: EPTCS 351, 2021, pp. 242-259

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

Authors: Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, Ichiro Hasuo

Abstract: 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 resul… ▽ 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, 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. △ Less

Submitted 21 May, 2021; originally announced May 2021.

Comments: 14 pages + 9 page appendix, to appear in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021)

Learning Pomset Automata

Authors: Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Alexandra Silva

Abstract: 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. 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. △ Less

Submitted 15 February, 2021; originally announced February 2021.

Journal ref: Proc. FoSSaCS 2021, pp 510-530

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

Authors: Ornela Dardha, Jurriaan Rot

Abstract: This volume contains the proceedings of EXPRESS/SOS 2020: the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational Semantics, which was held online, as an affiliated workshop of CONCUR 2020, the 31st International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in th… ▽ More This volume contains the proceedings of EXPRESS/SOS 2020: the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational Semantics, which was held online, as an affiliated workshop of CONCUR 2020, the 31st International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. △ Less

Submitted 27 August, 2020; originally announced August 2020.

Journal ref: EPTCS 322, 2020

Partially Observable Concurrent Kleene Algebra

Authors: Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, Alexandra Silva

Abstract: 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 observatio… ▽ 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 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. △ Less

Submitted 22 July, 2020; v1 submitted 15 July, 2020; originally announced July 2020.

Comments: Accepted for publication at CONCUR 2020

Journal ref: Proc. CONCUR 2020, 20:1-20:22

Expressive Logics for Coinductive Predicates

Authors: Clemens Kupke, Jurriaan Rot

Abstract: 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… ▽ More 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. △ Less

Submitted 14 December, 2021; v1 submitted 22 June, 2020; originally announced June 2020.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (December 15, 2021) lmcs:6593

Steps and Traces

Authors: Jurriaan Rot, Bart Jacobs, Paul 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 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. Ou… ▽ More 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. △ Less

Submitted 11 April, 2020; originally announced April 2020.

Up-to Techniques for Branching Bisimilarity

Authors: Rick Erkens, Jurriaan Rot, Bas Luttik

Abstract: Ever since the introduction of behavioral equivalences on processes one has been searching for efficient proof techniques that accompany those equivalences. Both strong bisimilarity and weak bisimilarity are accompanied by an arsenal of up-to techniques: enhancements of their proof methods. For branching bisimilarity, these results have not been established yet. We show that a powerful proof techn… ▽ More Ever since the introduction of behavioral equivalences on processes one has been searching for efficient proof techniques that accompany those equivalences. Both strong bisimilarity and weak bisimilarity are accompanied by an arsenal of up-to techniques: enhancements of their proof methods. For branching bisimilarity, these results have not been established yet. We show that a powerful proof technique is sound for branching bisimilarity by combining the three techniques of up to union, up to expansion and up to context for Bloom's BB cool format. We then make an initial proposal for casting the correctness proof of the up to context technique in an abstract coalgebraic setting, covering branching but also η, delay and weak bisimilarity. △ Less

Submitted 24 January, 2020; originally announced January 2020.

Journal ref: Extended abstract published in the proceedings of SOFSEM 2020, LNCS 12011, pages 285 - 297, Springer

Preservation of Equations by Monoidal Monads

Authors: Louis Parlant, Jurriaan Rot, Alexandra Silva, Bas Westerbaan

Abstract: 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$)… ▽ 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$ 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. △ Less

Submitted 7 July, 2020; v1 submitted 17 January, 2020; originally announced January 2020.

A Categorical Framework for Learning Generalised Tree Automata

Authors: Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, Alexandra Silva

Abstract: 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 algebrai… ▽ 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. 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. △ Less

Submitted 2 May, 2022; v1 submitted 16 January, 2020; originally announced January 2020.

Journal ref: Proc. CMCS 2022, pp 67-87

Learning Weighted Automata over Principal Ideal Domains

Authors: Gerco van Heerdt, Clemens Kupke, Jurriaan Rot, Alexandra Silva

Abstract: In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal \LStar\ algorithm works when the semiring is a principal ideal domain, but not for general semirings such as the natural numbers. In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal \LStar\ algorithm works when the semiring is a principal ideal domain, but not for general semirings such as the natural numbers. △ Less

Submitted 14 October, 2021; v1 submitted 11 November, 2019; originally announced November 2019.

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

Authors: Jorge A. Pérez, Jurriaan Rot

Abstract: This volume contains the proceedings of EXPRESS/SOS 2019: the Combined 26th International Workshop on Expressiveness in Concurrency and the 16th Workshop on Structural Operational Semantics, which was held on August 26, 2019, in Amsterdam (The Netherlands), as an affiliated workshop of CONCUR 2019, the 30th International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at… ▽ More This volume contains the proceedings of EXPRESS/SOS 2019: the Combined 26th International Workshop on Expressiveness in Concurrency and the 16th Workshop on Structural Operational Semantics, which was held on August 26, 2019, in Amsterdam (The Netherlands), as an affiliated workshop of CONCUR 2019, the 30th International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. △ Less

Submitted 22 August, 2019; originally announced August 2019.

Journal ref: EPTCS 300, 2019

Separation and Renaming in Nominal Sets

Authors: Joshua Moerman, Jurriaan Rot

Abstract: 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 nom… ▽ More 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. △ Less

Submitted 3 June, 2019; originally announced June 2019.

Completeness and Incompleteness of Synchronous Kleene Algebra

Authors: Jana Wagemaker, Marcello Bonsangue, Tobias Kappé, Jurriaan Rot, Alexandra Silva

Abstract: Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then… ▽ More Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics. △ Less

Submitted 16 July, 2019; v1 submitted 21 May, 2019; originally announced May 2019.

Comments: Accepted at MPC 2019

Journal ref: Proc. MPC 2019, pp 385-413

Tree Automata as Algebras: Minimisation and Determinisation

Authors: Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, Alexandra Silva

Abstract: We study a categorical generalisation of tree automata, as $Σ$-algebras for a fixed endofunctor $Σ$ 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… ▽ More We study a categorical generalisation of tree automata, as $Σ$-algebras for a fixed endofunctor $Σ$ 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. △ Less

Submitted 16 July, 2019; v1 submitted 18 April, 2019; originally announced April 2019.

Journal ref: Proc. CALCO 2019, pp 6:1-6:22

Fast Computations on Ordered Nominal Sets

Authors: David Venhoek, Joshua Moerman, Jurriaan Rot

Abstract: We show how to compute efficiently with nominal sets over the total order symmetry, by develo** 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 n… ▽ More We show how to compute efficiently with nominal sets over the total order symmetry, by develo** 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. △ Less

Submitted 16 August, 2022; v1 submitted 22 February, 2019; originally announced February 2019.

Coalgebra Learning via Duality

Authors: Simone Barlocco, Clemens Kupke, Jurriaan Rot

Abstract: 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… ▽ More 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. △ Less

Submitted 8 August, 2019; v1 submitted 15 February, 2019; originally announced February 2019.

Kleene Algebra with Observations

Authors: Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, Fabio Zanasi

Abstract: 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 al… ▽ 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 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. △ Less

Submitted 21 August, 2019; v1 submitted 16 November, 2018; originally announced November 2018.

Journal ref: Proc. CONCUR 2019, pp 41:1-41:16

Bisimilarity of Open Terms in Stream GSOS

Authors: Filippo Bonchi, Tom van Bussel, Matias David Lee, Jurriaan Rot

Abstract: Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main co… ▽ More Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main contribution is to capture equivalence of open terms as bisimilarity on certain Mealy machines, providing a concrete proof technique. Moreover, we introduce an enhancement of this technique, called bisimulation up-to substitutions, and show how to combine it with other up-to techniques to obtain a powerful method for proving equivalence of open terms. △ Less

Submitted 12 February, 2019; v1 submitted 8 November, 2018; originally announced November 2018.

Journal ref: Science of Computer Programming, Volume 172, pages 1-26, 2019, Elsevier

Coalgebraic Determinization of Alternating Automata

Authors: Meven Bertrand, Jurriaan Rot

Abstract: 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 auto… ▽ More 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. △ Less

Submitted 7 April, 2018; originally announced April 2018.

ACM Class: F.3.2; F.4.1

Companions, Causality and Codensity

Authors: Damien Pous, Jurriaan Rot

Abstract: 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 distr… ▽ More 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. △ Less

Submitted 7 August, 2019; v1 submitted 22 December, 2017; originally announced December 2017.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (August 8, 2019) lmcs:4166

Distributive Laws for Monotone Specifications

Authors: Jurriaan Rot

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… ▽ More 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. △ Less

Submitted 4 September, 2017; originally announced September 2017.

Comments: In Proceedings EXPRESS/SOS 2017, arXiv:1709.00049

Journal ref: EPTCS 255, 2017, pp. 83-97

Coalgebraic trace semantics via forgetful logics

Authors: Bartek Klin, Jurriaan Rot

Abstract: 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 determiniza… ▽ More 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. △ Less

Submitted 27 December, 2016; v1 submitted 16 November, 2016; originally announced November 2016.

ACM Class: F.3.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2622

Learning Minimum Volume Sets and Anomaly Detectors from KNN Graphs

Authors: Jonathan Root, Venkatesh Saligrama, **g Qian

Abstract: We propose a non-parametric anomaly detection algorithm for high dimensional data. We first rank scores derived from nearest neighbor graphs on $n$-point nominal training data. We then train limited complexity models to imitate these scores based on the max-margin learning-to-rank framework. A test-point is declared as an anomaly at $α$-false alarm level if the predicted score is in the $α$-percen… ▽ More We propose a non-parametric anomaly detection algorithm for high dimensional data. We first rank scores derived from nearest neighbor graphs on $n$-point nominal training data. We then train limited complexity models to imitate these scores based on the max-margin learning-to-rank framework. A test-point is declared as an anomaly at $α$-false alarm level if the predicted score is in the $α$-percentile. The resulting anomaly detector is shown to be asymptotically optimal in that for any false alarm rate $α$, its decision region converges to the $α$-percentile minimum volume level set of the unknown underlying density. In addition, we test both the statistical performance and computational efficiency of our algorithm on a number of synthetic and real-data experiments. Our results demonstrate the superiority of our algorithm over existing $K$-NN based anomaly detection algorithms, with significant computational savings. △ Less

Submitted 22 January, 2016; originally announced January 2016.

Comments: arXiv admin note: substantial text overlap with arXiv:1502.01783, arXiv:1405.0530

Presenting Distributive Laws

Authors: Marcello M. Bonsangue, Helle Hvid Hansen, Alexander Kurz, Jurriaan Rot

Abstract: 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 t… ▽ 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 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. △ Less

Submitted 5 August, 2015; v1 submitted 9 March, 2015; originally announced March 2015.

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 3 (August 7, 2015) lmcs:1578

Learning Efficient Anomaly Detectors from $K$-NN Graphs

Authors: **g Qian, Jonathan Root, Venkatesh Saligrama

Abstract: We propose a non-parametric anomaly detection algorithm for high dimensional data. We score each datapoint by its average $K$-NN distance, and rank them accordingly. We then train limited complexity models to imitate these scores based on the max-margin learning-to-rank framework. A test-point is declared as an anomaly at $α$-false alarm level if the predicted score is in the $α$-percentile. The r… ▽ More We propose a non-parametric anomaly detection algorithm for high dimensional data. We score each datapoint by its average $K$-NN distance, and rank them accordingly. We then train limited complexity models to imitate these scores based on the max-margin learning-to-rank framework. A test-point is declared as an anomaly at $α$-false alarm level if the predicted score is in the $α$-percentile. The resulting anomaly detector is shown to be asymptotically optimal in that for any false alarm rate $α$, its decision region converges to the $α$-percentile minimum volume level set of the unknown underlying density. In addition, we test both the statistical performance and computational efficiency of our algorithm on a number of synthetic and real-data experiments. Our results demonstrate the superiority of our algorithm over existing $K$-NN based anomaly detection algorithms, with significant computational savings. △ Less

Submitted 5 February, 2015; originally announced February 2015.

Comments: arXiv admin note: text overlap with arXiv:1405.0530

Coinduction up to in a fibrational setting

Authors: Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot

Abstract: 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 coind… ▽ 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 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. △ Less

Submitted 15 May, 2014; v1 submitted 26 January, 2014; originally announced January 2014.

Journal ref: CSL-LICS, Vienne : France (2014)

Interacting via the Heap in the Presence of Recursion

Authors: Jurriaan Rot, Irina Măriuca Asăvoae, Frank de Boer, Marcello M. Bonsangue, Dorel Lucanu

Abstract: 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… ▽ 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 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. △ Less

Submitted 16 December, 2012; originally announced December 2012.

Comments: In Proceedings ICE 2012, arXiv:1212.3458

ACM Class: F.1.1, F.1.2, F.3.1, F.3.3

Journal ref: EPTCS 104, 2012, pp. 99-113

On the specification of operations on the rational behaviour of systems

Authors: Marcello M. Bonsangue, Stefan Milius, Jurriaan Rot

Abstract: 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 functo… ▽ More 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. △ Less

Submitted 13 August, 2012; originally announced August 2012.

Comments: In Proceedings EXPRESS/SOS 2012, arXiv:1208.2440

Journal ref: EPTCS 89, 2012, pp. 3-18