Space-time process algebra with asynchronous communication
J. A. Bergstra, C. A. Middelburg
TL;DR
This work develops Space-Time Process Algebra (STPA), an ACP-based formalism for modeling timed, spatially distributed systems with asynchronous communication that avoids the integration (variable-binding) operator. It introduces a purely equational time/space domain—the signed meadow with square root—and uses state operators to model asynchronous data flow, together with absolute and relative timing, a time-out operator, and maximal progress to capture priorities. The paper provides a complete axiom system, structural operational semantics, and bisimilarity theory, along with guarded recursion and an instructive PAR-style data communication protocol example. It also proves soundness and (semi-)completeness results, and discusses extensions such as spatial movement and channel-rich replacements, underscoring STPA’s rigorous, algebraic foundation for space-time communication protocols. The framework enables precise reasoning about timing constraints, broadcasting data, and protocol correctness in distributed systems with spatial distribution.
Abstract
We introduce a process algebra that concerns the timed behaviour of distributed systems with a known spatial distribution. This process algebra provides a communication mechanism that deals with the fact that a datum sent at one point in space can only be received at another point in space at the point in time that the datum reaches that point in space. The variable-binding integration operator used in related process algebras to model such a communication mechanism is absent from this process algebra. This is considered an advantage because the variable-binding operator does not really fit in with an algebraic approach and a process algebra with this operator is not firmly founded in established metatheory.