Abstract: Implication algebras are known to be axiomatised by a finite number of equations (making the representation and finite representation problems decidable in that case). We show that this also holds in the context of unary (and binary) relations and present a Stone-style representation theorem. We then show that the (finite) representation decision problem is undecidable for implication semigroups, in stark contrast with implication algebras.

Abstract: We present a lattice of distributed program specifications, whose ordering represents implementability/refinement.
Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock.
This is to overcome fundamental physical difficulties with synchronisation.
The lattice of specifications is assembled and analysed with several established mathematical tools.
Sets of nondegenerate cells of a simplicial set model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness.
The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al.
In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport's definition of sequential consistency.
The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion.
The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.

Abstract: In this paper, we consider relational structures arising from Comer's finite field construction, where the cosets need not be sum free. These Comer schemes generalize the notion of a Ramsey scheme and may be of independent interest. As an application, we give the first finite representation of $34_{65}$. We complement our upper bounds with some lower bounds. Using a SAT solver, we establish that $33_{65}$ is not representable on fewer than $24$ points and $34_{65}$ is not representable on fewer than $24$ points.

Abstract: Using computer software, every quantale on up to nine elements has been enumerated up to isomorphism, catalogued and classified with respect to various properties. In order to achieve this the enumeration was branched by partitioning the search space based on various isomorphic invariants of quantales.

Abstract: Units of measure with prefixes and conversion rules are given a formal semantic model in terms of categorial group theory. Basic structures and both natural and contingent semantic operations are defined. Conversion rules are represented as a class of ternary relations with both group-like and category-like properties. A hierarchy of subclasses is explored, with increasingly benign algebraic behavior, culminating in a direct efficient conversion-by-rewriting algorithm.

Abstract: Freyd categories provide a semantics for first-order effectful programming languages by capturing the two different orders of evaluation for products. We enrich Freyd categories in a duoidal category, which provides a new, third choice of parallel composition. Duoidal categories have two monoidal structures which account for the sequential and parallel compositions. The traditional setting is recovered as a full coreflective subcategory for a judicious choice of duoidal category. We give several worked examples of this uniform framework, including the parametrised state monad, basic separation semantics for resources, and interesting cases of change of enrichment.

Abstract: We prove that the equational theory of *-continuous Kleene algebra with domain is EXPTIME-complete. Our proof makes essential use of Hollenberg's equational axiomatization of program equations valid in relational test algebra.

Abstract: We show the following dependences between relational domain constructions in the framework of heterogeneous relation algebras. If all power sets and subsets exist and objects are comparable, then all sums exist. If all sums exist and atoms are rectangular, then all products exist. If all atoms are rectangular, then all subsets exist if and only if all quotients exist. We give models with rectangular atoms which rule out further dependences between these constructions.

Abstract: This paper is concerned with the refinement and control of a certain class of labelled transition systems, called plant automata, via bisimulation quotients.
Refinement means that arbitrary transitions may be removed whereas control allows only removing edges with the same edge label.
The goal is to ensure given LTL properties in the resulting plant automaton.
We give a hardness result for refinement and control and investigate, in particular, the question whether refineability and controllability can be decided by looking at bisimulation quotients.

Abstract: BL-algebras are the algebraic semantics of Basic logic BL, the logic of all continuous t-norms and their residua. In a previous work, we provided the classification of the amalgamation property (AP) for the varieties of BL-algebras generated by one BL-chain with finitely-many components. As an open problem, we left the analysis of the AP for varieties of BL-algebras generated by one finite set of BL-chains with finitely-many components. In this paper we provide a partial solution to this problem. We provide a classification of the AP for the varieties of BL-algebras generated by one finite set of BL-chains with finitely-many components, which are either cancellative hoops or finite Wajsberg hoops. We also discuss the difficulties to generalize this approach to the more general case.

Abstract: Kleene Algebra (KA) is the algebra of regular expressions. Central to the study of KA is Kozen's (1994) completeness result, which says that any equivalence valid in the language model of KA follows from the axioms of KA. Also of interest is the finite model property (FMP), which says that false equivalences always have a finite counterexample. Palka (2005) showed that, for KA, the FMP is equivalent to completeness.

We provide a unified and elementary proof of both properties. In contrast with earlier completeness proofs, this proof does not rely on minimality or bisimilarity techniques for deterministic automata. Instead, our approach avoids deterministic automata altogether, and uses Antimirov's derivatives and the well-known transition monoid construction.

Our results are fully verified in the Coq proof assistant.

Abstract: The tensor product (K (x) C2') of the *-continuous Kleene algebra K with the polycyclic *-continuous Kleene algebra C2' of two bracket pairs contains a copy of the fixed-point closure of K: the centralizer of C2' in (K (x) C2'). We prove a representation of elements of (K (x) C2') by automata a la Kleene and refine it by normal form theorems that restrict the occurrences of brackets on paths through the automata. This is the basis for a calculus of context-free expressions.

Abstract: We address algebraic aspects of invariant generation and proving termination, two central questions of program analysis, for non-deterministic loops with polynomial updates.

Our focus is sketching the boundary of (un-)decidability for both problems between different classes of programs. The first main contribution of this work is related to the question raised by Braverman in 2006: ``How much non-determinism can be introduced in a linear loop before termination becomes undecidable?'' We show that termination of loops with a purely non-deterministic choice between linear updates is undecidable in the presence of linear inequality loop conditions.

In the context of invariants, an algorithm is known that computes all polynomial relations among variables of loops with multiple linear updates. At the same time, allowing polynomial assignments of higher degrees was shown to result in algorithmic unsolvability. We highlight that negative results in fact do not exploit general polynomial updates. We show that no algorithm can find all polynomial relations for programs as soon as quadratic updates or updates guarded by affine equalities are involved.

Abstract: We show that every locally integral involutive partially ordered monoid (ipo-monoid) $\mathbf A = (A,\le, \cdot, 1, \sim, -)$, and in particular every locally integral involutive semiring, decomposes in a unique way into a family $\{\mathbf A_p : p\in A^+\}$ of integral ipo-monoids, which we call its \emph{integral components}. In the semiring case, the integral components are semirings. Moreover, we show that there is a family of monoidal homomorphisms $\Phi = \{\varphi_{pq}\colon \mathbf A_p\to \mathbf A_q : p\leq q\}$, indexed on the positive cone $(A^+,\leq)$, so that the structure of $\mathbf A$ can be recovered as a glueing $\int_\Phi \mathbf A_p$ of its integral components along $\Phi$. Reciprocally, we give necessary and sufficient conditions so that the P\l{}onka sum of any family of integral ipo-monoids $\{\mathbf A_p : p\in D\}$, indexed on a lower-bounded join-semilattice $(D,\vee, 1)$, along a family of monoidal homomorphisms $\Phi$ is an ipo-monoid.

Abstract: In this paper we start the investigation of an object representing the real numbers in categories of relations. Our axiomatization uses the construction of a relation power, i.e., an abstract version of power sets within the category. This allows us to utilize a relation algebraic version of Tarski's axioms of the real numbers as a first-order definition of a real number object. The current paper focuses on the addition operation of the real number object. It is shown that addition forms a densely and linearly ordered abelian group.

Abstract: We present a general method for computing vector representations $\Fr$ of sets of relations. This method is used for obtaining $\Fr$ from an inclusion $\FR \subseteq \FS$, where $\FR$ and $\FS$ are relation-algebraic expressions over a relation
rather than its vector representation. The core of the method is a theorem that shows how $\Fr$ can be obtained from $\FR \subseteq \FS$ in one step. As applications we consider some problems concerning kernels of relations.

Abstract: Weakening relations are all binary relations defined on a poset such that the partial order acts as a both-sided compositional identity. This is motivated by the weakening rule in sequent calculi and closely related to models of relevance logic. For a fixed poset the collection of weakening relations is a subreduct of the full relation algebra on the underlying set of the poset. We present a two-player game for the class of representable weakening relation algebras akin to that for the class of representable relation algebras. This enables us to define classes of abstract weakening relation algebras that approximate the quasivariety of representable weakening relation algebras. We give explicit finite axiomatisations for some of these classes. We define the class of diagonally representable weakening relation algebras and prove that it is a discriminator variety. We also provide explicit representations for several small weakening relation algebras.