Order algebras: a quantitative model of interaction

TL;DR

This paper introduces order algebras, a quantitative, non-interleaving model of concurrent interaction that uses linear combinations of partial orders to faithfully interpret process algebras and extend testing semantics.

Contribution

It presents a novel algebraic framework called order algebras that models non-determinism and concurrency in a denotational, non-interleaving manner, connecting to differential linear logic.

Findings

Provides a faithful interpretation of finitary process algebras.

Extends testing semantics to a quantitative, non-interleaving setting.

Shows algebraic constructions form a structure akin to differential linear logic.

Abstract

A quantitative model of concurrent interaction is introduced. The basic objects are linear combinations of partial order relations, acted upon by a group of permutations that represents potential non-determinism in synchronisation. This algebraic structure is shown to provide faithful interpretations of finitary process algebras, for an extension of the standard notion of testing semantics, leading to a model that is both denotational (in the sense that the internal workings of processes are ignored) and non-interleaving. Constructions on algebras and their subspaces enjoy a good structure that make them (nearly) a model of differential linear logic, showing that the underlying approach to the representation of non-determinism as linear combinations is the same.