Behavioural theories for concurrent actors

Abstract

In this work, we start by examining concurrent programming paradigms, specifically the actor model, and the challenges of formally ensuring that system refactorings preserve original behaviour. We explore the use of contextual behavioural theories to reason about these safety issues rigorously. While trace-based techniques are suggested as an improvement over the intractable nature of contextual testing, their inability to tractably reason about programs with an infinite number of traces prompts the need for another method of analysing actor systems. Furthermore, existing trace-based techniques use the notion of binding over traces to keep track of names, which becomes cumbersome as actor systems dynamically extrude names and grow in size. To address these gaps, this work presents a unified formal behavioural theory for concurrent actors. The primary contributions to knowledge include, first, the K | O ⊢ environment. This knowledge framework replaces trace binding by strictly enforcing the single-receiver property and elegantly handling dynamic name extrusion through defining known names and valid observer interfaces upfront. Second, we introduce an optimised trace preorder that restricts unobservable inputs, alongside a method for constructing a general observer. These results are required to demonstrate that trace techniques are both sound and complete with respect to safety testing. Finally, we present an asynchronous, set-based simulation. This framework based on coinductive reasoning is built to handle asynchronous actor systems that exhibit persistent behaviour and non-deterministic branching, allowing us to overcome the infinite-state analysis problem found in trace techniques, and simplifying the comparison of complex systems. Ultimately, these results establish a complete, provably equivalent behavioural theory that bridges contextual, trace-based, and coinductive preorders. This provides a scalable, mathematically rigorous model to safely verify system refactorings and component equivalence in modern, highly dynamic concurrent systems without the need for exhaustive testing.