Dynamic Effective Timed Communication Systems

Anoma Research Topics |TECHNICAL REPORT Dynamic Effective Timed Communication Systems Tobias Heindel a, Jonathan Prieto-Cubides a, and Anthony Harta aHeliax AG *E-Mail: [email protected], [email protected], [email protected]v Abstract Message passing concurrency is a widely used paradigm in distributed systems research. Communicating finite state machines (cfsm) are probably the simplest model of message passing concurrency—introduced in the eighties, but still the default model in the context of communication protocols, session types, and choreographies. Another well-known family of models are Agha’s actors, which populate the other end of the expressivity and complexity spectrum: actors may behave in ways that even go beyond the computable. We want to avoid the complexities of the actor model and separate out matters that go beyond the computable. Ideally, we want something as simple as cfsms to give semantics to engines of the Anoma specification but with adequate expressive power. This paper thus introduces a generalization of cfsms, called dynamic effective timed communication systems (detcs)—somewhat baroque but descriptive: they have arbitrary computable state transitions, can dynamically create new state machines, and come equipped with a clock for each machine. We retain the isolated turn principle of the actor model. Each machine performs “turns” one after the other: a turn is taking a waiting message, interpreting it, and deciding on both a state update for the machine and a collection of actions to take in response, perhaps sending messages or creating new machines.1The technical core of the paper is the definition of detcss an their labelled transition systems, which can be used to give operational semantics to engine systems of the Anoma specification. Keywords: Actor Model ; Distributed systems ; Time-stamped events ; Denotational semantics ; Temporal dependencies ; Enriched Event Diagrams ; (Received: February 24, 2025; Version: March 6, 2025) 1. Introduction Message passing concurrency is an established paradigm for modelling concurrent systems in order to reason about them with mathematical rigour. The basic idea of this paradigm is to put all agency and state into processes, which then communicate by exchanging messages with each other. The advantage is homogeneity, which is a bonus, in particular for reasoning about models. However, on the flip side, as all processes are created equal, it is potentially hard to distinguish between the purely computational aspects of a process and effects caused by agents operating under the guise of processes. In this paper, we present a generalization of communicating finite state machines (cfsm) that enables controlled interaction with human operators 1The wording is taken from [GJ16], replacing “actor” with “machine”. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |1–29 and external agents while preserving the simplicity of message passing concurrency, as detailed in Section 4.2. To the best of our knowledge, existing cfsm-based frameworks exhibit two key limitations for modelling realworld distributed protocols. First, current communication state-based systems models lack support for dynamic process creation —a limitation we address in Section 4.2. Second, they fail to properly incorporate clock-based timing mechanisms, as discussed in Section 4.3. The development of this work complements the ongoing development of the Anoma protocol [Co24]. In more detail, the paper generalizes cfsms in three ways: the state transition functions are arbitrary computable functions between countable sets; the number of communicating state machines is finite but may change dynamically, see Section 4.2; finally, transitions are timestamped by local clocks of the machines, see Section 4.3. We dub these systems dynamic effective timed communication systems since they are a generalization of the communication systems of [BLT20], state transitions are effective in the sense of computability theory, the number of process is dynamic, and we have local clocks to assign timestamps to incoming messages. In Section 5, we describe the main ideas of how we can obtain an interactive version, such that users can make decisions that need not be deterministic or computable from previous messages and the local state. Concerning related work, the connection to communicating finite state machines is already covered by the above description. The main conceptual difference to the actor model [Agh86b] is the separation of the purely computational aspects of actors and other sources of agency. Machines take care of the computational parts, but everything else is pushed outside the system; the system interacts with the environment via channels, for which it may be natural to assume stronger synchrony assumptions than the default assumptions of distributed systems (namely, asynchrony or partial synchrony). The remainder of this paper is structured as follows. We first revise the background material on message passing concurrency and review the Token Ring Protocol (standardized as ieee 802.5), which will serve as our running example in Section 2. Then we describe conventions of notation and the relevant elements of computability theory in Section 3. After that, we come to the technical core of the paper, culminating in the definition of detcss and their labelled transition semantics (see Definition 12), in Section 4. The mechanism for channels through which the system can be affected by external agents is described in Section 5. Finally, we discuss related work and conclude. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |2 2. Background: communicating processes and protocols The main protagonist of the paper is a model of computation2for processes with local clocks, which may communicate according to some protocol—or not.3The purpose of the computational model is to enable reasoning about such sets of timed processes. Our approach is based on state machines, a common basic abstraction in computer science. The slogan is: the simpler the model, the better for protocol design! We thus review the most important context before defining the model itself: we start with the definition of the term “protocol”, followed by some simple examples for protocol implementation that involve communicating processes—directly or implicitly. 2.1. Protocol generalities: communication protocol definition We take the following text-book definition of “protocol” [Her20] as a reference point: a set of rules which determine how two or more entities should communicate is called a communication protocol, or protocol for short. The point we want to emphasize is the normative aspects of protocols: protocols are about the admissible sets of messages that each participant may send at a given point in time and they describe which messages a participant should accept under which circumstances and act accordingly. Let us look at the Anoma Protocol [Co24] for an example that illustrates the normative character of protocols: one desired property is that each user request for matching an intent or settlement of a transaction should be considered by the collective of operators of the Anoma instance (leading to matching or settlement with adequate speed, if possible). However, in the present paper, we are mainly concerned with the actual communication that entities engage in; the reason is that we first want to agree on a framework for how to reason about implementation candidates for a protocol before we start addressing the question of how we can check that a set of observed message exchanges adheres to the protocol. 2.2. Protocol generalities: protocol instances In the present paper, we want to distinguish between protocols, specifying desired communication patterns, and something else that concerns the actual 2Please be assured, the authors would rather take a model of computation off the shelf instead of going through the ordeal of comparing with the literature (see also Section 6). There simply seems no model out there that strikes a useful compromise between the simplicity of communicating (finite) state machines and the expressive power of the actor model, while providing a local wall-clock time for each protocol participant. In particular, there seems to be no good match with any the four categories proposed in Ref. [DKVCDM16], especially when it comes to user interactions as described in Section 5. 3We discuss protocols informally in Section 2.1. Let us point out here, once more, that the question of what a protocol is “exactly” is out of scope. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |3 communications performed. Let us formulate a candidate definition: A protocol instance is the actual message passing of processes that conforms to a protocol. (1) The main variations of such a notion of protocol instance concern the nature of message passing and the assumptions about the participating processes. Concerning message passing, we shall follow the usual paradigm of eventual delivery of messages; concerning processes, we aim for a variation on the theme of actors, but restricted in suitable ways so that they can be implemented on a general purpose computer. The model of computation that we describe takes communicating finite state machines [BZ83] as a starting point for a generalization. There are also similarities and indirect influences from the co-algebraic description of object oriented systems [Jac95]. However, the present paper aims to keep matters as basic as possible. Matters of fault tolerance will be covered in future versions of the paper. 2.3. Communicating processes: abstract and concrete descriptions A communicating process, not necessarily in the context of a protocol, can be described abstractly as a function that takes a stream of inputs and produces astream of outputs. In the case of communicating finite state machines, this conversion is described concretely, using state updates, transforming inputs to outputs, one letter at a time4However, abstractly, the communication between the processes described by a set of communicating finite state machines arises by the suitable connection of input streams to output streams. In the case of cfsms, this “wiring” between processes is fixed in advance and stays forever. In distributed systems research, it is common to abstract away the details of how output streams relate to input streams through a generic communication network. 2.4. Last but not least: the communication network How does a message “travel” between the communicating processes? The idea is to refrain from answering this question! We assume a generic asynchronous communication network, as is common in distributed systems research. The only assumption is that each message that is sent will be receivable at the destination, eventually. In other words, each message that can be read from an output stream will eventually be processed as part of the input stream of the process that is the destination of the message. In the original work on communicating finite state machines [BZ83], the network was required to preserve the order of messages, i.e., the network 4A related notion is that of transducer in automata theory. Also note that this very much fits the idea of the Isolated Turn Principle [DKVCDM16]. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |4 could be described as a clique of pair-wise fifo channels. We drop the assumption that message order is preserved, which is the usual assumption in distributed systems. We only postulate that the network routes one message at a time, taking a message out of one of the output streams and delivering it to the corresponding input stream, e.g., by pushing it to the recipient’s “inbox”-queue.5 2.5. Example protocols: token-ring variations A common family of examples for illustrating communication protocols is based on The Token Ring Protocol, standardized as ieee 802.5. This protocol assumes a fixed set of processes that are organized in a ring topology. The station 1 station 2 station 3 station 4 interfaces Figure 1. Token ring illustration (based on [MV93]). main idea of the Token Ring Protocol is to allow every process to send, from time to time, a data payload to every other process in a fixed ring topology, disseminating the data one hop at a time around the ring until it arrives again at the sender (which then can check that the message was transmitted correctly); in the terminology of this protocol, this is a data frame (see also [MV93]). When a bit arrives at a ring-interface it is copied into a 1-bit buffer and then put into the ring again. While in the buffer, the bit can be inspected and possibly modified before being written out into the ring again. To this end, an “idle”-token is circulated until some participant in the ring stops circulating the “idle”-token and starts transmitting a message. 5The case of dynamic creation of new processes is more challenging in that we essentially have to extend processes with streams of spawning requests and an “operator” that actually creates the system. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |5 2.6. Miscellaneous notes to the reader In this paper, we only consider flat protocols. Aspects of non-trivial protocol structure are left for future work. We are agnostic to how the rules of communications are given in a protocol, simply because the question of correctness of protocol instantiation are out of scope. One guiding motive of the paper is the question of how we can avoid the yet another programming language-trap and keep a direct relation to communicating finite state machines [BZ83] (see also Appendix A). This will in particular concern the setting where processes are supposed to spawn new processes. We do not propose a programming language for this. 3. Notation and conventions In definitions, we use the symbol ≔to introduce new terminology and/or notation: the symbols to the left are the ones that are to be defined in terms of symbols to the right. Generally speaking, we follow established conventions of the computer science community, e.g., Nis the set of natural numbers including zero. For the sake of clarity, we recall notation and conventions that we use in the paper. Capital letters denote sets unless stated otherwise. Thus, the letters 𝐴 and 𝐵stand for sets (making no claim about whether 𝐴and 𝐵are equal). Set inclusion is denoted by ⊆,i.e., we write 𝐴⊆𝐵when every element of 𝐴 belongs to 𝐵; the empty set is denoted by ∅. The Cartesian product of a pair of sets 𝐴,𝐵is denoted by 𝐴×𝐵, and ordered pairs of elements 𝑎,𝑏 are written ⟨𝑎,𝑏⟩,i.e., ⟨𝑎,𝑏⟩ ∈ 𝐴×𝐵if, and only if, 𝑎∈𝐴and 𝑏∈𝐵. The zeroary Cartesian product is denoted by 1={⟨⟩}. Given two sets 𝐴, 𝐵, their union is 𝐴∪𝐵and their disjoint union is 𝐴+𝐵≔𝐴× {0} ∪ 𝐴× {1}. Two disjoint sets 𝐴and 𝐵are said to be disjoint if 𝐴∩𝐵=∅. The cardinality of a set 𝐴 is denoted by #(𝐴). The power set of a set 𝐴is denoted by Powerset(𝐴); the set of all finite subsets of a set 𝐴is Powersetfin(𝐴),i.e., Powersetfin(𝐴)≔{𝐿⊆𝐴|#(𝐿) ∈ N}. A relation between sets 𝐴and 𝐵is a subset of the Cartesian product 𝐴×𝐵in which 𝐴is called the domain of the relation and 𝐵its codomain. A relation 𝑅⊆𝐴×𝐵is a partial map when for each element 𝑎∈𝐴, there is at most one element 𝑏∈𝐵such that ⟨𝑎,𝑏⟩ ∈ 𝑅; we write 𝜑:𝐴⇀𝐵, when 𝜑is a partial map from 𝐴to 𝐵. A partial map 𝜑:𝐴⇀𝐵is defined for an element 𝑎∈𝐴when ⟨𝑎,𝑏⟩ ∈ 𝜑for some element 𝑏∈𝐵; whenever 𝜑 is defined for 𝑎∈𝐴, then 𝜑(𝑎)denotes the unique element of 𝐵such that ⟨𝑎, 𝜑 (𝑎)⟩ ∈ 𝜑. The domain of definition of a partial map is denoted by df (𝜑),i.e., df (𝜑)≔{𝑎∈𝐴| ∃𝑏∈𝐵. ⟨𝑎,𝑏⟩ ∈ 𝜑}. We write 𝜑:𝐴. −⇀𝐵when 𝜑is a partial map from 𝐴to 𝐵with finite domain of definition. A function DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |6 is a partial map whose domain of definition coincides with its entire domain; we write 𝑓:𝐴→𝐵when 𝑓is a function with domain 𝐴and codomain 𝐵. The set of all functions from 𝐴to 𝐵is 𝐵𝐴,i.e., 𝐵𝐴≔{𝑓∈Powerset(𝐴×𝐵) | 𝑓:𝐴→𝐵}. We use postfix notation for the projection function of each product of a Cartesian product, i.e., −1:𝐴×𝐵→𝐴−2:𝐴×𝐵→𝐵, and thus, we have ⟨𝑎,𝑏⟩1=𝑎and ⟨𝑎,𝑏⟩2=𝑏, for every ⟨𝑎,𝑏⟩ ∈ 𝐴×𝐵. Implementability via computability theory. We want to make sure that the machines that we shall introduce (see Definition 1) are actually implementable. For this, we appeal to the usual apparatus of computability theory [Tur37b,RJ67].6A partial recursive function between sets 𝐴and 𝐵 is a partial map 𝜑:𝐴⇀𝐵that can be implemented by a Turing machine [Tur37b], a lambda calculus term [Tur37a], or a program that is written in the reader’s favourite programming language as long as it takes elements of 𝐴as input and either outputs elements of 𝐵if the input was part of the domain of definition or runs forever if it was not part of the domain of definition. For every countable set 𝐴, we assume a “reasonable”7injective function [_]:𝐴→N, called the encoding of the set 𝐴. We denote the image of the set 𝐴as subset of the natural numbers as [𝐴] ⊆ N. Sometimes, it is important that the set [𝐴]is decidable,i.e., it must be decidable whether an element 𝑥∈Nbelongs to [𝐴](and not to N\ [𝐴]), which, in turn, means that there exists a partial computable function 𝜒:N→ {0,1}that computes 1on input 𝑥iff 𝑥∈ [𝐴]. Finally, we are using the fact that we can enumerate computable functions between sets in a suitable way, known as admissible indexing [RJ67, Example 2-10], i.e., a numbering of computable functions that allows to represent every computable function that moreover satisfies Kleene’s 𝑆𝑚 𝑛-theorem [Kle52]. 4. Communication systems of effective Moore machines In this section, we generalize communicating finite state machines [BZ83] in three steps: 1. We define a variation of Moore’s sequential machines [Moo56]; 2. We add a mechanism for spawning new machines, dynamically; 6These matters are technically important, but may be skipped safely on a first reading. 7We want to elide the details of how elements of sets are represented as natural numbers. Unfortunately, for definitions to be well-defined, we must encode inputs and outputs to make them machine readable. Things become easier if we simply assume that every relevant set actually is a subset of the natural numbers; then, we do not need to worry about details of encoding sets. If that is too drastic for the reader’s taste, we can equip each set 𝐴with an encoding that is computable and total, using a definition of computability in terms of Turing machines [HMU01] and the usual binary encoding of the natural numbers. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |7 3. We equip each machine with its own clock. We choose Moore machines as our state machine model instead of Mealy machines because they simplify the semantics. With Moore machines, one can clearly separate a machine’s internal state transitions from its overall effects that it has on the system, making the definition of the basic labelled transition semantics much more straightforward (see Definition 8).8 Sequential machines à la Moore, but with computable behaviour. Moore’s description of sequential machines [Moo56] contains an explanation of what he means by deterministic behaviour, namely that the present state of a machine depends only on its previous input and previous state, and the present output depends only on the present state. We want to keep this description, but remove the restriction to finite sets that Moore imposes when writing [Moo56] that the sequential machines considered have a finite number of states, a finite number of possible input symbols, and a finite number of possible output symbols. This paper aims for the most straightforward generalization of Moore’s sequential machines whose behaviour is computable9. Dynamic creation of new machines. We also want to model the dynamic creation of new machines as a new “action primitive”, in addition to the usual sending and receiving of messages in protocol instances (cf. transmissions and receptions, resp. [BZ83]). Hence, we augment the output set of our generalized Moore machines so that machines can make requests to spawn new machines, much like how a process can spawn child processes. This feature is directly analogous to actor creation [Agh86b]. Spawning a new machine requires a piece of “source code”10 that describes the behaviour of the new machine, along with an “address” at which the machine will be available (see Definition 6 for more details). These “addresses” will be called participant IDs (pid), mainly to make the relation to the terminology of choreography automata [BLT20] evident.11 8We describe in Section 5 how user interactions can be incorporated into the Moore-esque approach. 9We shall use the usual mathematical definitions of partial recursive functions [Com] that has become established to capture the intuition of what is effectively calculable. 10In ABCL/1, these source code snippets are called scripts. 11Incidentally, it is “not entirely wrong” to read pid as process ID, which is used to reference an Erlang/Elixir process. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |8 Wall-clock timestamps for every message. The third and final step consists of adding a clock for every participating machine. In more detail, each incoming message is stamped at the moment of reception with the receiving machine’s wall-clock time. Using local timestamps, we can implement busy waiting12 (by sending messages to self). More interestingly, wall-clock time-stamps can be used to measure latency, round-trip times, and the like. 4.1. Moore-esque machines with computable behaviour We first define a generalization of Moore’s sequential machine that matches his description of deterministic behaviour [Moo56]; then, we follow up with the desired restriction to computable behaviour, which we dub effective Moore machines (see Definition 3). Definition 1 (Moore-esque machine).Relative to two fixed sets Σand Γ, a Moore-esque machine with input alphabet Σand output alphabet Γis a quadruple ⟨𝑄,𝑞0, 𝛿, 𝜇⟩, consisting of • a set of states 𝑄, • a current state 𝑞0∈𝑄, • a state transition map 𝛿:𝑄×Σ⇀𝑄, and • an output map 𝜇:𝑄⇀Γ. For any Moore-esque machine 𝔪, we denote its state set, current state, transition map, and output map by States𝔪,s𝔪,in𝔪, and out𝔪, respectively. Finally, given a Moore-esque machine 𝔪 = ⟨𝑄, 𝑞0, 𝛿, 𝜇⟩and a state 𝑞∈𝑄, we define the state substitution ⟨𝑄,𝑞0, 𝛿, 𝜇⟩@𝑞≔⟨𝑄, 𝑞, 𝛿, 𝜇⟩, which reads “𝔪at state 𝑞.” send 1 listen 0 copy 𝑥 𝑥≠0 1 𝑥≠0 0 0 Figure 2. A Moore-esque machine 12A “native” timer mechanism is described in Appendix B, which comes at the price of somewhat complex notation and lengthy definitions. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |9 E E E E Figure 5. Wall-clocks at each station. A sendΔ,𝑘,𝑡 AB!Δ listenΔ,𝑘 AB!0 copy AB!𝑥BA?𝑥(𝑥≠0) BA?Δ, 𝑡′ 𝑘++ Δ:=𝑘Δ+(𝑡′−𝑡) 𝑘+1 BA?𝑥(𝑥≠0) BA?0, 𝑡 BA?0 However, there is no guarantee that the average round-trip time will converge, since we are considering a fully asynchronous setting. Therefore, without additional assumptions about the “delivery speed” of the network, we cannot make any guesses about the relative speeds of clocks, since the network may be “infinitely slow” or slowing down due to a growing number of participants. We now extend the labelled transition semantics of decss under modest assumptions about the network and clocks, namely, that every message will be available for reception and that messages take at least one clock cycle to be received. The only difference in message reception is the additional timestamp, which the receiving machine may take into consideration (or ignore). Note that we must use an adapted machine encoding J𝑛K′′ Athat handles the changes in the input and output alphabets of emms. Definition 12 (Labelled transition system of a detcs).A DETCS-state is defined as a triple ⟨𝑆,𝑊 , 𝑀⟩, such that the first two components together form a detcs and the last component is a finite set of transmissions 𝑀∈ Powersetfin(ÐA∈df (𝑆)TA). Given a detcs-state ⟨𝑆,𝑊 , 𝑀⟩, a transmission AB!m∈𝑀, and a strictly positive delay 0<𝑡∈N,the AB!m-𝑡-successor DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |16 of ⟨𝑆,𝑊 , 𝑀⟩is the detcs-state ⟨ˆ 𝑆, ˆ 𝑊 , ˆ 𝑀⟩where ˆ 𝑆(C)=                         𝑆(B)@in𝑆(B)s𝑆(B),⟨𝑡′,AB?m⟩ where 𝑡′=𝑊(B) + 𝑡 if C=B, 𝑆(C)if C∈df (𝑆) \ {B}, J𝑛K′′ Cif B𝑛∗C∈outˆ 𝑆(B)(sˆ 𝑆(B)) and C∉df (𝑆), undefined otherwise —this is in direct analogy to the definition for the case without clocks, but augmented by the “time stamp” 𝑡′of the newly arrived message—and we have the following definition for updating clocks: ˆ 𝑊(C)=                   𝑊(B) + 𝑡if B=C 𝑊(C)if C∈df (𝑆) \ {B}, 0if B𝑛∗C∈outˆ 𝑆(B)(sˆ 𝑆(B)) and C∉df (𝑆). undefined otherwise. ˆ 𝑀=(𝑀\ {AB!m}) ∪ outˆ 𝑆(B)(sˆ 𝑆(B)) ∩ T B, i.e., the clock of the receiving machine is incremented by an arbitrary positive delay, all other clocks are unaffected, except for newly spawned clocks that are initialized to 0. A labelled transition between detcs-states ⟨𝑆,𝑊 , 𝑀⟩and ⟨ˆ 𝑆, ˆ 𝑊 , ˆ 𝑀⟩is a quadruple D⟨𝑆,𝑊 , 𝑀⟩,AB!m, 𝑡, ⟨ˆ 𝑆, ˆ 𝑊 , ˆ 𝑀⟩E, such that ⟨ˆ 𝑆, ˆ 𝑊 , ˆ 𝑀⟩is the AB!m-𝑡-successor of ⟨𝑆,𝑊 , 𝑀⟩. Finally, the LTS of DETCS-states is the lts ⟨𝑋, →⟩ whose set of states 𝑋is the set of detcsstates and the labelled transition relation →is the set of all labelled transitions between detcs-states. We write ⟨𝑆,𝑊 , 𝑀⟩AB!m −−−−→ 𝑡⟨ˆ 𝑆, ˆ 𝑊 , ˆ 𝑀⟩ when ⟨ˆ 𝑆, ˆ 𝑊 , ˆ 𝑀⟩is the AB!m-𝑡-successor of ⟨𝑆,𝑊 , 𝑀⟩. Remark 13 (Non-deterministic message delivery).Messages are delivered completely asynchronously, possibly including the re-ordering of messages (although this cannot happen in the examples). Additional assumptions about the message delivery can be made later on. Roughly, the scheduling is demonic non-determinism, not controlled by the system, but by the network operator. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |17 model state machine dynamic time user I/O cfsm dfa × × × ecs emm × × × decs emm ✓× × detcs emm ✓ ✓ × detcis ecimm ✓ ✓ ✓ Figure 6. Comparison matrix of computational models for protocol instantiation. 5. Make it talk to the world: synchronous I/O interfaces Conceptually, we are still in a closed world, because the development is starting from communicating finite state machines. This is why, so far, we could not meaningfully model the actual token ring protocol, because we are missing the possibility to read the data to send from the stations (and in a synchronous manner). We now sketch how we add the missing link to the environment, which makes it possible to model the original token ring protocol using the interactive version of communicating systems. To open up our systems and make them talk to the world, we introduce an interface for communication with users, external hardware, and other input/output agents in the environment (from the perspective of the machine). One way to make the system open is as follows: first, we assume that interaction with the local environment is synchronous (e.g., the user is prompted whenever an important message arrives); second, we take the simplest possible interface, considering only one prompt in each isolated turn. This approach is sufficient to offer the user a complete interaction automaton with finite state space, which could be given as a traditional Moore machine with synchronous input and output. This approach is inspired by read–eval–print loops (repls): the machine prompts the local environment for input whenever it needs to make choices or read data. It then evaluates the data, transitions to the next state, and waits for the next message to arrive (after sending messages and spawning machines based on the new state).19 In the example of the Token Ring, the interaction with the station is used to fill up memory with a payload for the next turn of a partaking process in the Token Ring Protocol. Let us describe in more detail how we can add interactivity to Moore-esque machines. For every received message AB?m, there may arise the need to request input from the environment. Whenever such input is required, the machine produces a signal $𝑧—in analogy to the print part in a repl—that depends on the received message AB?mand the current state. The environment then produces a data item 𝑥in response to the prompt; e.g., this could be an answer to a multiple choice question or input that follows a regular expression pattern. Finally, the machine processes the message-data pair 19This approach is compatible with a seamless user experience, as the user may be notified asynchronously about what has happened, using a message to itself. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |18 ⟨AB?m, 𝑥⟩to advance to the next state, then sends messages and spawns new machines. Thus, in our definition, for each participant A, we additionally need a set of signals SA, a set of data X, and a map of type 𝑄× RA⇀SAthat outputs a signal to which the environment is expected to respond, synchronously. To formalize the synchronous communication, we suppose that each machine is connected with the environment via an input stream; then a choice of the environment is given by a map from signals $𝑧∈ SAto data 𝑥∈X.20 We augment the interaction labels to have the shape AB!m.𝑥, representing a message reception ⟨AB?m, 𝑥⟩and input data 𝑥∈X, which was read from the environment in response to receiving the message AB!m. Accordingly, we could define the following generalization of Moore-esque machines. Definition 14 (Moore-esque machine with interfaces).Relative to four sets Σ,Γ,Ψ,Ξ, a Moore-esque machine with interfaces with input alphabet Σ, output alphabet Γ, signal alphabet Ψ, and data alphabet Ξ, is a quintuple ⟨𝑄,𝑞0, 𝛿, 𝜌, 𝜇⟩, consisting of • a set of states 𝑄, • an current state 𝑞0∈𝑄, • a signal map 𝜌:𝑄×Σ⇀Ψ, • a state transition map 𝛿:𝑄×Σ×Ξ⇀𝑄, and • an output map 𝜇:𝑄⇀Γ. In summary, this means that whenever the machine is to react according to a received message, the machine will start an interaction “through” the I/O stream with whatever entities are on the “other side” of the I/O, be it a user, a specific hardware device, or anything that is within the same location and thus allows for synchronous communication. With this variation of Moore-esque machines at hand, we plan to capture the case of synchronous interaction with the environment, i.e., the last line in Figure 6. This brings into the picture synchronous variations of the actor model. 6. Related work Communication systems [BLT20] bear obvious family resemblances with actor models [Agh86b,Agh86a]. The proposed detcss are a minor variation of communication systems—at least if we take a step back to look at the big picture;in particular, they inherit the family resemblances. The main motivation for writing up a machine-based model is that we want to avoid committing to any specific one of the multitude of actor models, but rather have a suitable abstraction for all of them. 20This input stream can be optional, and in principle two machines could share such input streams. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |19 Let us consider some specific points to make the relation between actor models and communicating systems clearer.21 First, a labelled transition semantics has also been given to actor systems [AMST97]. If we summarize several transitions of the latter into macro-steps [DKVCDM16], we obtain a close correspondence between these macro-steps of actor systems and labelled transitions of detcss. Moreover, we can also make a connection to Clinger’s interaction diagrams [Cli81]: each path in the lts of a detcs that leads to a state with an empty message set corresponds to an interaction diagram with one event per labelled transition. In summary, the main point is that if we seriously consider the Isolated Turn Principle (itp) [DKVCDM16]— shared by all actor models—we can think of the lts semantics as the counterpart of the itp for detcss as there is a bijective relation between labelled transitions on the one hand and turns performed by machines on the other hand.22 Turning to more application-oriented work, there is a specific line of research that aims to bring session types [HYC08] to actor languages. Roughly, session types refine interfaces (in the sense of actor systems [DKVCDM16]), which describe which messages an actor is ready to process at any given point in time. Let us point out ElixirST [FT23] as one specific example of this line of research. ElixirST comes with a labelled transition semantics that is slightly more fine-grained, as it also considers outputs and, more importantly, function calls. However, the input labels of both ltss correspond to each other directly. More generally, it seems hard to find a model of distributed message-passing systems that allows for Turing-complete computational processes and user interactions while being described independently of a specific programming language. Naturally, all early actor languages, such as ABCL/1 [YBS86], come with a built-in scripting language. However, even more recent general frameworks, such as timed Rebeca [ACI+11], introduce specific syntax to describe process behaviour. A production-ready approach is safe asynchronous event-driven programming in P[DGJ+13]. However, here again, the focus is not on a general model but rather on a specific way to enable asynchronous computation. A short overview of the wider context is given in a recent position paper [FHK+24]. 7. Conclusion We proposed detcss as a model of distributed computation that lies between the presentation of actor models and communicating finite state machines, including a timed labelled transition semantics. Instead of inventing yet another process description language, we presented a direct generalization 21A fully fledged comparison to the actor model is beyond the scope of the paper. 22Here, we abstract away from any substrate on which machines are running. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |20 of communicating finite state (Moore) machines, using concepts from computability theory. Precisely, we elaborated semantics for two new main features: the dynamic creation of processes, Section 4.2, and the use of clocks, Section 4.3. These are necessary to reason about general protocols. To complete the picture, in Section 5, we sketched how we can incorporate synchronous interactions with the environment, allowing machines “to talk to the outside world” [Arm02]. The main open task for future work is to study the relationship between choreographies, session types, and other mechanisms and calculi for protocol specification and implementation. The direct next step consists of filling in the details of user interactions, especially for the timed setting, in a way that matches existing programming languages in common use. A related topic is reasoning about the communication in a system as observed by a fixed set of “monitors” and how it relates to message logic [GZ24]. Further directions include structured systems with components or modules (see e.g., [GY23]), fault tolerance, and distributed runtime verification of protocols. Acknowledgements. We would like to thank Murdoch James Gabbay for his clearly stated advice for how to improve the paper. References ACI+11. Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, Arni Hermann Reynisson, Steinar Hugi Sigurdarson, and Marjan Sirjani. Modelling and simulation of asynchronous real-time systems using timed rebeca. Electronic Proceedings in Theoretical Computer Science, 58:1–19, July 2011. URL: http://dx.doi.org/ 10.4204/EPTCS.58.1,doi:10.4204/eptcs.58.1. (cit. on p. 20.) Agh86a. Gul Agha. An overview of actor languages. SIGPLAN Not., 21(10):58–67, jun 1986. doi:10.1145/323648.323743. (cit. on p. 19.) Agh86b. Gul A. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986. (cit. on pp. 2,8, and 19.) AMST97. Gul A. Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott. A foundation for actor computation. J. Funct. Program., 7(1):1–72, January 1997. doi:10.1017/S095679689700261X. (cit. on p. 20.) APS14. Matteo Avalle, Alfredo Pironti, and Riccardo Sisto. Formal verification of security protocol implementations: a survey. Formal Aspects of Computing, 26:99–123, 2014. Arm97. Joe Armstrong. The development of erlang. SIGPLAN Not., 32(8):196–203, aug 1997. doi:10.1145/258949.258967. Arm02. Joe Armstrong. Getting erlang to talk to the outside world. In Proceedings of the 2002 ACM SIGPLAN Workshop on Erlang, ERLANG ’02, page 64–72, New York, NY, USA, 2002. Association for Computing Machinery. doi:10.1145/ 592849.592858. (cit. on p. 21.) BCG+21. Alessandro Bruni, Marco Carbone, Rosario Giustolisi, Sebastian Mödersheim, and Carsten Schürmann. Security Protocols as Choreographies, pages 98–111. Springer International Publishing, Cham, 2021. doi:10.1007/ 978-3-030-91631-2_5. BCK01. Paolo Baldan, Andrea Corradini, and Barbara König. A static analysis techDOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |21 nique for graph transformation systems. In International Conference on Concurrency Theory, pages 381–395. Springer, 2001. (cit. on p. 13.) BLT20. Franco Barbanera, Ivan Lanese, and Emilio Tuosto. Choreography automata. In Simon Bliudze and Laura Bocchi, editors, Coordination Models and Languages, pages 86–106, Cham, 2020. Springer International Publishing. (cit. on pp. 2,8,10,11,12,19, and 26.) BP16. Carlos Baquero and Nuno Preguiça. Why logical clocks are easy: Sometimes all you need is the right language. Queue, 14(1):53–69, feb 2016. doi:10. 1145/2898442.2917756. BP19. Tomasz Brengos and Marco Peressotti. Behavioural equivalences for timed systems. Logical Methods in Computer Science, Volume 15, Issue 1, February 2019. URL: https://lmcs.episciences.org/5220,doi:10.23638/LMCS-15(1:17) 2019. BZ83. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983. (cit. on pp. 4,6,7,8, and 26.) CL85. K. Mani Chandy and Leslie Lamport. Distributed snapshots: determining global states of distributed systems. ACM Transactions on Computer Systems, 3(1):63–75, feb 1985. doi:10.1145/214451.214456. Cli81. William Douglas Clinger. Foundations of Actor Semantics. PhD thesis, Massachusetts Institute of Technology (MIT), 1981. URL: https://dspace.mit.edu/ handle/1721.1/6935. (cit. on p. 20.) Co24. Anoma Contributors and others. Anoma Specification v0.1.4, 2024. URL: https://github.com/anoma/nspec. (cit. on pp. 2and 3.) Com. Computable function. http://encyclopediaofmath.org/index.php?title= Computable_function&oldid=41830. retrieved 11 Nov. 2024. (cit. on p. 8.) DGJ+13. Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. P: safe asynchronous event-driven programming. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, page 321–332, New York, NY, USA, 2013. Association for Computing Machinery. doi:10.1145/2491956. 2462184. (cit. on p. 20.) DKVCDM16. Joeri De Koster, Tom Van Cutsem, and Wolfgang De Meuter. 43 years of actors: a taxonomy of actor models and their key properties. In Proceedings of the 6th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE 2016, page 31–40, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/3001886.3001890. (cit. on pp. 3,4, and 20.) FAS+23. Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder. Special delivery: Programming with mailbox types. Proceedings of the ACM on Programming Languages, 7(ICFP):78–107, August 2023. URL: http://dx.doi.org/10.1145/3607832,doi:10.1145/3607832. FHK+24. Simon Fowler, Philipp Haller, Roland Kuhn, Sam Lindley, Alceste Scalas, and Vasco T. Vasconcelos. Behavioural types for heterogeneous systems (position paper). Electronic Proceedings in Theoretical Computer Science, 401:37–48, April 2024. URL: http://dx.doi.org/10.4204/EPTCS.401.4,doi:10.4204/eptcs. 401.4. (cit. on p. 20.) FT23. Adrian Francalanza and Gerard Tabone. Elixirst: A session-based type system for elixir modules. Journal of Logical and Algebraic Methods in Programming, 135:100891, 2023. URL: https://www.sciencedirect.com/science/article/ pii/S2352220823000457,doi:10.1016/j.jlamp.2023.100891. (cit. on p. 20.) Gir94. Jean-Yves Girard. Light linear logic. In International Workshop on Logic and Computational Complexity, pages 145–176. Springer, 1994. (cit. on p. 15.) GJ16. Tony Garnock-Jones. History of actors. https://eighty-twenty.org/2016/10/ 18/actors-hopl, Oct 2016. Accessed 24th of Februrary 2025. (cit. on p. 1.) Göd31. Kurt Gödel. Über formal unentscheidbare sätze der principia mathematica DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |22 und verwandter systeme i. Monatshefte für mathematik und physik, 38:173– 198, 1931. (cit. on p. 12.) Gur00. Yuri Gurevich. Sequential abstract-state machines capture sequential algorithms. ACM Transactions on Computational Logic (TOCL), 1(1):77–111, 2000. GY23. Lorenzo Gheri and Nobuko Yoshida. Hybrid multiparty session types – full version, 2023. URL: https://arxiv.org/abs/2302.01979,arXiv:2302.01979. (cit. on p. 21.) GZ24. Murdoch J. Gabbay and Naqib Zarin. Message Logic. Anoma Research Topics, Dec 2024. URL: https://doi.org/10.5281/zenodo.14251397,doi:10.5281/ zenodo.14251398. (cit. on p. 21.) HBS73. Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI’73, page 235–245, San Francisco, CA, USA, 1973. Morgan Kaufmann Publishers Inc. Her20. Drago Hercog. Communication protocols: principles, methods and specifications. Springer Nature, 2020. (cit. on p. 3.) Hew07. Carl Hewitt. What is commitment? physical, organizational, and social (revised). In Pablo Noriega, Javier Vázquez-Salceda, Guido Boella, Olivier Boissier, Virginia Dignum, Nicoletta Fornara, and Eric Matson, editors, Coordination, Organizations, Institutions, and Norms in Agent Systems II, pages 293–307, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. HMU01. John E Hopcroft, Rajeev Motwani, and Jeffrey D Ullman. Introduction to automata theory, languages, and computation. Acm Sigact News, 32(1):60– 65, 2001. (cit. on p. 7.) HYC08. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLANSIGACT symposium on Principles of programming languages, pages 273–284, 2008. (cit. on p. 20.) IS14. Shams M. Imam and Vivek Sarkar. Selectors: Actors with multiple guarded mailboxes. In Proceedings of the 4th International Workshop on Programming Based on Actors Agents & Decentralized Control, AGERE! ’14, page 1–14, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/ 2687357.2687360. Jac95. Bart Jacobs. Objects and classes, co-algebraically. In Object orientation with parallelism and persistence, pages 83–103. Springer, 1995. (cit. on p. 4.) JR97. Bart Jacobs and Jan Rutten. A tutorial on (co) algebras and (co) induction. Bulletin-European Association for Theoretical Computer Science, 62:222–259, 1997. Kle52. Stephen Cole Kleene. Introduction to Metamathematics. P. Noordhoff N.V., Groningen, 1952. (cit. on p. 7.) KP04. Marco Kick and John Power. Modularity of behaviours for mathematical operational semantics. Electronic Notes in Theoretical Computer Science, 106:185–200, 2004. Lam78. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558–565, jul 1978. doi:10.1145/359545.359563. LY19. Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, pages 97–117, Cham, 2019. Springer International Publishing. Mal95. Grant Malcolm. Behavioural equivalence, bisimulation, and minimal realisation. In Workshop on the Specification of Abstract Data Types, pages 359–378. Springer, 1995. Mil89. R. Milner. Communication and Concurrency. Prentice-Hall, Inc., USA, 1989. Mon23. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, 2023. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |23 Moo56. Edward F. Moore. Gedanken-Experiments on Sequential Machines, pages 129–154. Princeton University Press, Princeton, 1956. URL: https: //doi.org/10.1515/9781400882618-006 [cited 2024-11-19], doi:doi:10.1515/ 9781400882618-006. (cit. on pp. 7,8, and 9.) MV93. S. Mauw and G. J. Veltink, editors. Algebraic specification of communication protocols. Cambridge University Press, USA, 1993. (cit. on p. 5.) RJ67. Hartley Rogers Jr. Theory of recursive functions and effective computability. McGraw-Hill Book Company, 1967. (cit. on pp. 7and 12.) Sch90. Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv., 22(4):299–319, December 1990. doi:10.1145/98163.98167. SHC+23. Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming (ECOOP 2023), volume 263 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1–29:29, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https: //drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.29,doi: 10.4230/LIPIcs.ECOOP.2023.29. She15. Justin Sheehy. There is no now: Problems with simultaneity in distributed systems. Queue, 13(3):20–27, mar 2015. doi:10.1145/2742694.2745385. SS76. Dana Scott and Christopher Strachey. Toward a Mathematical Semantics for Computer Languages. Prentice-Hall, 1976. Stu24. Felix Stutz. Implementability of Asynchronous Communication Protocols - The Power of Choice. PhD thesis, Kaiserslautern University of Technology, Germany, 2024. URL: https://kluedo.ub.rptu.de/frontdoor/index/index/docId/ 8077. Tal98. Carolyn L. Talcott. Composable semantic models for actor theories. Higher Order Symbolic Computation, 11(3):281–343, 1998. URL: http://dx.doi.org/10. 1023/A:1010042915896,doi:10.1023/a:1010042915896. TF21. Gerard Tabone and Adrian Francalanza. Session types in elixir. In Proceedings of the 11th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE 2021, page 12– 23, New York, NY, USA, 2021. Association for Computing Machinery. doi: 10.1145/3486601.3486708. Tur37a. A. M. Turing. Computability and 𝜆-definability. Journal of Symbolic Logic, 2(4):153–163, 1937. doi:10.2307/2268280. (cit. on p. 7.) Tur37b. A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230– 265, 1937. URL: https://londmathsoc.onlinelibrary.wiley.com/doi/abs/10. 1112/plms/s2-42.1.230,arXiv:https://londmathsoc.onlinelibrary.wiley. com/doi/pdf/10.1112/plms/s2-42.1.230,doi:10.1112/plms/s2-42.1.230. (cit. on p. 7.) XZH+19. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in coq. Proceedings of the ACM on Programming Languages, 4(POPL):1–32, December 2019. URL: http://dx.doi.org/10. 1145/3371119,doi:10.1145/3371119. YBS86. Akinori Yonezawa, Jean-Pierre Briot, and Etsuya Shibayama. Objectoriented concurrent programming in abcl/1. In Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications, OOPSLA ’86, page 258–268, New York, NY, USA, 1986. Association for Computing Machinery. doi:10.1145/28697.28722. (cit. on p. 20.) YW15. Shohei Yasutake and Takuo Watanabe. Actario: A framework for reasoning about actor systems. In Workshop on Programming based on Actors, Agents, DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |24 and Decentralized Control (AGERE), 2015. DOI: 10.5281/zenodo.14984148 Anoma Research Topics |March 6, 2025 |25