32 citations · 119 across the 15 of their papers we have counts for
16 papers
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity
Wojciech Różowski, Tobias Kappé, Dexter Kozen +2
We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branc…
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Tobias Kappé, Todd Schmid, Alexandra Silva
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…
An Elementary Proof of the FMP for Kleene Algebra
Tobias Kappé
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.…
Formal Abstractions for Packet Scheduling
Anshuman Mohan, Yunhe Liu, Nate Foster +2
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 f…
A Categorical Framework for Learning Generalised Tree Automata
Gerco van Heerdt, Tobias Kappé, Jurriaan Rot +2
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 diff…
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Steffen Smolka, Nate Foster, Justin Hsu +3
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 pre…
Completeness and Incompleteness of Synchronous Kleene Algebra
Jana Wagemaker, Marcello Bonsangue, Tobias Kappé +2
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 lo…
Tree Automata as Algebras: Minimisation and Determinisation
Gerco van Heerdt, Tobias Kappé, Jurriaan Rot +2
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 cat…
On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata
Tobias Kappé, Paul Brunet, Bas Luttik +2
Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operation…
Kleene Algebra with Observations
Tobias Kappé, Paul Brunet, Jurriaan Rot +3
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 s…
Equivalence checking for weak bi-Kleene algebra
Tobias Kappé, Paul Brunet, Bas Luttik +2
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 ca…
Decision problems for Clark-congruential languages
Makoto Kanazawa, Tobias Kappé
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-co…
Concurrent Kleene Algebra: Free Model and Completeness
Tobias Kappé, Paul Brunet, Alexandra Silva +1
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 wi…
A Component-oriented Framework for Autonomous Agents
Tobias Kappé, Farhad Arbab, Carolyn Talcott
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 meanin…
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages
Tobias Kappé, Paul Brunet, Bas Luttik +2
Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the f…
A Compositional Framework for Preference-Aware Agents
Tobias Kappé, Farhad Arbab, Carolyn Talcott
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…