Finite representability of semigroups with demonic refinement

The motivation for using demonic calculus for binary relations stems from the behaviour of demonic turing machines, when modelled relationally. Relational composition (;) models sequential runs of two programs and demonic refinement (⊑) arises from the partial order given by modeling demonic choice (⊔) of programs (see below for the formal relational definitions). We prove that the class R(⊑ , ;) of abstract (≤ , ∘) structures isomorphic to a set of binary relations ordered by demonic refinement with composition cannot be axiomatised by any finite set of first-order (≤ , ∘) formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines R(⊑ , ;). We prove that a finite representable (≤ , ∘) structure has a representation over a finite base. This appears to be the first example of a signature for binary relations with composition where the representation class is non-finitely axiomatisable, but where the finite representation property holds for finite structures.