Showing 1–25 of 25 results for author: Kappé, T

A General Completeness Theorem for Skip-free Star Algebras

Authors: Tobias Kappé, Todd Schmid

Abstract: We consider process algebras with branching parametrized by an equational theory T, and show that it is possible to axiomatize bisimilarity under certain conditions on T. Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS'20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness… ▽ More We consider process algebras with branching parametrized by an equational theory T, and show that it is possible to axiomatize bisimilarity under certain conditions on T. Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS'20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness results. △ Less

Submitted 25 January, 2025; originally announced January 2025.

Algebras for Deterministic Computation Are Inherently Incomplete

Authors: Balder ten Cate, Tobias Kappé

Abstract: Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic programming constructs (sequencing, non-deterministic choice, and iteration) it is able to express all non-deterministic finite state control flow over a finite set of primitives. It is natural to ask whether there exists… ▽ More Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic programming constructs (sequencing, non-deterministic choice, and iteration) it is able to express all non-deterministic finite state control flow over a finite set of primitives. It is natural to ask whether there exists a similar finite set of constructs that can capture all deterministic computation. We show that this is not the case. More precisely, the deterministic fragment of KAT is not generated by any finite set of regular control flow operations. This generalizes earlier results about the expressivity of the traditional control flow operations, i.e., sequential composition, if-then-else and while. △ Less

Submitted 16 January, 2025; v1 submitted 21 November, 2024; originally announced November 2024.

CF-GKAT: Efficient Validation of Control-Flow Transformations

Authors: Cheng Zhang, Tobias Kappé, David E. Narváez, Nico Naus

Abstract: Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break, and return. To overc… ▽ More Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break, and return. To overcome these limitations, we introduce Control-Flow GKAT (CF-GKAT), a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT's abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren's goto-elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation. △ Less

Submitted 16 January, 2025; v1 submitted 20 November, 2024; originally announced November 2024.

Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity

Authors: Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, Alexandra Silva

Abstract: We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimi… ▽ More We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in $O(n^3 \log n)$ time via a generic partition refinement algorithm. △ Less

Submitted 2 May, 2023; originally announced May 2023.

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

Authors: Tobias Kappé, Todd Schmid, Alexandra Silva

Abstract: Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa's axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results fo… ▽ More Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa's axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT consisting of skip-free programs. △ Less

Submitted 1 October, 2024; v1 submitted 26 January, 2023; originally announced January 2023.

An Elementary Proof of the FMP for Kleene Algebra

Authors: Tobias Kappé

Abstract: Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, it integrates well with interactive theorem provers. This raises the question: which equations can we (not) prove using the laws of KA? Moreover, which models of KA are complete, in the sense that they satisfy exactly the provable equations? Kozen (1994) answered these qu… ▽ More Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, it integrates well with interactive theorem provers. This raises the question: which equations can we (not) prove using the laws of KA? Moreover, which models of KA are complete, in the sense that they satisfy exactly the provable equations? Kozen (1994) answered these questions by characterizing KA in terms of its language model. Concretely, equivalences provable in KA are exactly those that hold for regular expressions. Pratt (1980) observed that KA is complete w.r.t. relational models, i.e., that its provable equations are those that hold for any relational interpretation. A less known result due to Palka (2005) says that finite models are complete for KA, i.e., that provable equivalences coincide with equations satisfied by all finite KAs. Phrased contrapositively, the latter is a finite model property (FMP): any unprovable equation is falsified by a finite KA. Both results can be argued using Kozen's theorem, but the implication is mutual: given that KA is complete w.r.t. finite (resp. relational) models, Palka's (resp. Pratt's) arguments show that it is complete w.r.t. the language model. We embark on a study of the different complete models of KA, and the connections between them. This yields a novel result subsuming those of Palka and Pratt, namely that KA is complete w.r.t. finite relational models. Next, we put an algebraic spin on Palka's techniques, which yield a new elementary proof of the finite model property, and by extension, of Kozen's and Pratt's theorems. In contrast with earlier approaches, this proof relies not on minimality or bisimilarity of automata, but rather on representing the regular expressions involved in terms of transformation automata. △ Less

Submitted 10 August, 2024; v1 submitted 21 December, 2022; originally announced December 2022.

Formal Abstractions for Packet Scheduling

Authors: Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, Dexter Kozen

Abstract: Early programming models for software-defined networking (SDN) focused on basic features for controlling network-wide forwarding paths, but more recent work has considered richer features, such as packet scheduling and queueing, that affect performance. In particular, PIFO trees, proposed by Sivaraman et al., offer a flexible and efficient primitive for programmable packet scheduling. Prior work h… ▽ More Early programming models for software-defined networking (SDN) focused on basic features for controlling network-wide forwarding paths, but more recent work has considered richer features, such as packet scheduling and queueing, that affect performance. In particular, PIFO trees, proposed by Sivaraman et al., offer a flexible and efficient primitive for programmable packet scheduling. Prior work has shown that PIFO trees can express a wide range of practical algorithms including strict priority, weighted fair queueing, and hierarchical schemes. However, the semantic properties of PIFO trees are not well understood. This paper studies PIFO trees from a programming language perspective. We formalize the syntax and semantics of PIFO trees in an operational model that decouples the scheduling policy running on a tree from the topology of the tree. Building on this formalization, we develop compilation algorithms that allow the behavior of a PIFO tree written against one topology to be realized using a tree with a different topology. Such a compiler could be used to optimize an implementation of PIFO trees, or realize a logical PIFO tree on a target with a fixed topology baked into the hardware. To support experimentation, we develop a software simulator for PIFO trees, and we present case studies illustrating its behavior on standard and custom algorithms. △ Less

Submitted 19 October, 2023; v1 submitted 21 November, 2022; originally announced November 2022.

ACM Class: C.2.1; E.1

Leapfrog: Certified Equivalence for Protocol Parsers

Authors: Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett

Abstract: We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a bisimulation, using "leaps." Proofs are powered by a certified compilation chain from first-order entailments to low-level bitvector verification conditions, which are di… ▽ More We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a bisimulation, using "leaps." Proofs are powered by a certified compilation chain from first-order entailments to low-level bitvector verification conditions, which are discharged using off-the-shelf SMT solvers. As a result, parser equivalence proofs in Leapfrog are fully automatic and push-button. We mechanically prove the core metatheory that underpins our approach, including the key transformations and several optimizations. We evaluate Leapfrog on a range of practical case studies, all of which require minimal configuration and no manual proof. Our largest case study uses Leapfrog to perform translation validation for a third-party compiler from automata to hardware pipelines. Overall, Leapfrog represents a step towards a world where all parsers for critical network infrastructure are verified. It also suggests directions for follow-on efforts, such as verifying relational properties involving security. △ Less

Submitted 18 May, 2022; originally announced May 2022.

Journal ref: Proc. PLDI 2022, 950-965

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

Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

Authors: Todd Schmid, Tobias Kappé, Dexter Kozen, Alexandra Silva

Abstract: Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebr… ▽ More Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to behaviors of GKAT expressions. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms. △ Less

Submitted 20 May, 2021; v1 submitted 16 February, 2021; originally announced February 2021.

Comments: 32 pages

Journal ref: Proc. ICALP 2021, pp 142:1-142:14

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

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

Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness

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

Abstract: Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $\mathsf{while}$-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In th… ▽ More Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $\mathsf{while}$-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA "with hypotheses", of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO. △ Less

Submitted 22 February, 2020; originally announced February 2020.

Journal ref: Proc. FoSSaCS 2020, pp 381-400

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

Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time

Authors: Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, Alexandra Silva

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

Submitted 13 December, 2019; v1 submitted 12 July, 2019; originally announced July 2019.

Comments: Extended version with appendix

Journal ref: Proc. POPL 2020, pp 61:1-61:28

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

On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata

Authors: Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, Fabio Zanasi

Abstract: Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operational perspectives is important, for both foundations and applications. This paper takes an important step towards such a correspondence, by precisely relating bi-Kleene Algebra (BKA), a fragment of CKA, to a novel type of… ▽ More Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operational perspectives is important, for both foundations and applications. This paper takes an important step towards such a correspondence, by precisely relating bi-Kleene Algebra (BKA), a fragment of CKA, to a novel type of automata, pomset automata (PAs). We show that PAs can implement the BKA semantics of series-parallel rational expressions, and that a class of PAs can be translated back to these expressions. We also characterise the behavior of general PAs in terms of context-free pomset grammars; consequently, universality, equivalence and series-parallel rationality of general PAs are undecidable. △ Less

Submitted 14 December, 2018; v1 submitted 7 December, 2018; originally announced December 2018.

Comments: Accepted manuscript

Journal ref: J. Log. Algebraic Methods Program. 103, pp 130-153, 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

Equivalence checking for weak bi-Kleene algebra

Authors: Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, Fabio Zanasi

Abstract: Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-ratio… ▽ More Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable. △ Less

Submitted 11 August, 2021; v1 submitted 5 July, 2018; originally announced July 2018.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 3 (August 13, 2021) lmcs:7502

Decision problems for Clark-congruential languages

Authors: Makoto Kanazawa, Tobias Kappé

Abstract: A common question when studying a class of context-free grammars is whether equivalence is decidable within this class. We answer this question positively for the class of Clark-congruential grammars, which are of interest to grammatical inference. We also consider the problem of checking whether a given CFG is Clark-congruential, and show that it is decidable given that the CFG is a DCFG. A common question when studying a class of context-free grammars is whether equivalence is decidable within this class. We answer this question positively for the class of Clark-congruential grammars, which are of interest to grammatical inference. We also consider the problem of checking whether a given CFG is Clark-congruential, and show that it is decidable given that the CFG is a DCFG. △ Less

Submitted 21 August, 2018; v1 submitted 11 May, 2018; originally announced May 2018.

Comments: Version 2 incorporates revisions prompted by the comments of anonymous referees at ICGI and LearnAut

Journal ref: PMLR 93 (Proc. ICGI 2018), pp 3-16

Concurrent Kleene Algebra: Free Model and Completeness

Authors: Tobias Kappé, Paul Brunet, Alexandra Silva, Fabio Zanasi

Abstract: 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. Moreo… ▽ 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 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 techniques developed along the way are reusable; in particular, they allow us to establish pomset automata as an operational model for CKA. △ Less

Submitted 26 February, 2018; v1 submitted 8 October, 2017; originally announced October 2017.

Comments: Version 2 includes an overview section that outlines the completeness proof, as well as some extra discussion of the interpolation lemma. It also includes better typography and a number of minor fixes. Version 3 incorporates the changes by comments from the anonymous referees at ESOP. Among other things, these include a worked example of computing the syntactic closure by hand

Journal ref: Proc. ESOP 2018, pp 856-882

A Component-oriented Framework for Autonomous Agents

Authors: Tobias Kappé, Farhad Arbab, Carolyn Talcott

Abstract: The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for… ▽ More The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for the component, while at design-time they can be used to reason about the behavior of the component in an uncertain physical world. Using structures that tell us how to compose preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system. We extend Linear Temporal Logic with two unary connectives that reflect the compositional structure of the actions, and show how it can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components. △ Less

Submitted 31 July, 2017; originally announced August 2017.

Journal ref: Proc. FACS 2017, pp 20-38

Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages

Authors: Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, Fabio Zanasi

Abstract: Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We pres… ▽ More Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours. △ Less

Submitted 22 October, 2017; v1 submitted 24 April, 2017; originally announced April 2017.

Comments: Version 2 incorporates changes prompted by comments of the anonymous referees at CONCUR. Besides minor corrections, this includes additions to the introduction and the discussion section, as well as a proof of Lemma 2.5. Version 3 corrects the accent on the first author's surname in the metadata

Journal ref: Proc. CONCUR 2017, pp 25:1-25:16

A Compositional Framework for Preference-Aware Agents

Authors: Tobias Kappé, Farhad Arbab, Carolyn Talcott

Abstract: A formal description of a Cyber-Physical system should include a rigorous specification of the computational and physical components involved, as well as their interaction. Such a description, thus, lends itself to a compositional model where every module in the model specifies the behavior of a (computational or physical) component or the interaction between different components. We propose a fra… ▽ More A formal description of a Cyber-Physical system should include a rigorous specification of the computational and physical components involved, as well as their interaction. Such a description, thus, lends itself to a compositional model where every module in the model specifies the behavior of a (computational or physical) component or the interaction between different components. We propose a framework based on Soft Constraint Automata that facilitates the component-wise description of such systems and includes the tools necessary to compose subsystems in a meaningful way, to yield a description of the entire system. Most importantly, Soft Constraint Automata allow the description and composition of components' preferences as well as environmental constraints in a uniform fashion. We illustrate the utility of our framework using a detailed description of a patrolling robot, while highlighting methods of composition as well as possible techniques to employ them. △ Less

Submitted 15 December, 2016; originally announced December 2016.

Comments: In Proceedings V2CPS-16, arXiv:1612.04023

Journal ref: EPTCS 232, 2016, pp. 21-35