Related papers: A Coalgebraic Approach to Kleene Algebra with Test…
Regular languages -- the languages accepted by deterministic finite automata -- are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. In this paper, we…
Typical arguments for results like Kleene's Second Recursion Theorem and the existence of self-writing computer programs bear the fingerprints of equational reasoning and combinatory logic. In fact, the connection of combinatory logic and…
Concurrent Kleene Algebra (CKA) is a recently proposed algebraic structure by Hoare and collaborators that unifies the laws of concurrent programming. The unifying power of CKA rests largely on the so-called exchange law that describes how…
Guarded Kleene Algebra with Tests (GKAT) is the fragment of Kleene Algebra with Tests (KAT) that arises by replacing the union and iteration operations of KAT with predicate-guarded variants. GKAT is more efficiently decidable than KAT and…
Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite state space utilising algebraic laws for reactive relations.…
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…
We show how concurrent quantales and concurrent Kleene algebras arise as convolution algebras $Q^X$ of functions from structures $X$ with two ternary relations that satisfy relational interchange laws into concurrent quantales or Kleene…
The theory of finite automata concerns itself with words in a free monoid together with concatenation and without further structure. There are, however, important applications which use alphabets which are structured in some sense. We…
We investigate the expressive power of regular expressions for languages of countable words and establish their expressive equivalence with logical and algebraic characterizations. Our goal is to extend the classical theory of regular…
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…
This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematical proofs. In…
Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories such as Concurrent Kleene Algebra, only partial correctness…
We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of…
We give a decision procedure and proof of correctness for the equational theory of probabilistic Kleene algebra with angelic nondeterminism introduced in Ong, Ma, and Kozen (2025).
One of the major open problems in automata and logic is the following: is there an algorithm which inputs a regular tree language and decides if the language can be defined in first-order logic? The goal of this paper is to present this…
Energy problems are important in the formal analysis of embedded or autonomous systems. Using recent results on star-continuous Kleene omega-algebras, we show here that energy problems can be solved by algebraic manipulations on the…
The Kleene theorem establishes a fundamental link between automata and expressions over the free monoid. Numerous generalisations of this result exist in the literature. Lifting this result to a weighted setting has been widely studied.…
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…
We develop a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphical representation as a two-dimensional syntax of string diagrams. Moreover, we provide an…
Automata admitting at most one accepting run per structure, known as unambiguous automata, find applications in verification of reactive systems as they extend the class of deterministic automata whilst maintaining some of their desirable…