Implication Algebras and Implication Semigroups of Binary Relations

Contextuality in distributed systems

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.

Comer Schemes, Relation Algebras, and the Flexible Atom Conjecture

Enumerating, Cataloguing and Classifying all Quantales on up to Nine Elements

Towards a Theory of Conversion Relations for Prefixed Units of Measure

Duoidally enriched Freyd categories

On the Complexity of *-Continuous Kleene Algebra With Domain

Dependences between Domain Constructions in Heterogeneous Relation Algebras

Compatibility of Refining and Controlling Plant Automata with 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.

Amalgamation property for some varieties of BL-algebras generated by one finite set of BL-chains with finitely-many components

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered

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.

Normal Forms for Elements of the *-Continuous Kleene Algebras K (x) C2'

What Else is Undecidable about Loops?

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.

The structure of locally integral involutive po-monoids and semirings

Relational Algebraic Approach to the Real Numbers - The Additive Group

A General Method for Representing Sets of Relations by Vectors

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.

Representable and diagonally representable weakening relation algebras