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

Recent Results on Component Twin-Width and Clique-Width with
Algorithmic Applications to Counting Graph Colorings

Translating First-Order Predicate Logic to Relation Algebra, an
Implementation

Model Synthesis based on Experience

Poset Product Representations Over Simple Residuated Lattices

Toward Ontology-based
Production - Relations building Airplanes

An Algebraic Representation of the Fixed-Point Closure of *-Continuous Kleene Algebras

Prenuclear vs. Nuclear Objects in ⋆-Autonomous Categories

Datalog with Equality: Semantics and Evaluation