Verifying Asynchronous Interactions via Communicating Session Automata
Abstract
This paper proposes a sound procedure to verify properties of communicating session automata (csa), i.e., communicating automata that include multiparty session types. We introduce a new asynchronous compatibility property for csa, called kmultiparty compatibility (kmc), which is a strict superset of the synchronous multiparty compatibility used in theories and tools based on session types. It is decomposed into two bounded properties: (i) a condition called ksafety which guarantees that, within the bound, all sent messages can be received and each automaton can make a move; and (ii) a condition called kexhaustivity which guarantees that all kreachable send actions can be fired within the bound. We show that kexhaustivity implies existential boundedness, and soundly and completely characterises systems where each automaton behaves equivalently under bounds greater than or equal to k. We show that checking kmc is pspacecomplete, and demonstrate its scalability empirically over large systems (using partial order reduction).
1 Introduction
Communicating automata are a Turingcomplete model of asynchronous interactions [10] that has become one of the most prominent for studying pointtopoint communications over unbounded firstinfirstout channels. This paper focuses on a class of communicating automata, called communicating session automata (csa), which strictly includes automata corresponding to asynchronous multiparty session types [28]. Session types originated as a typing discipline for the \(\pi \)calculus [27, 66], where a session type dictates the behaviour of a process wrt. its communications. Session types and related theories have been applied to the verification and specification of concurrent and distributed systems through their integration in several mainstream programming languages, e.g., Haskell [44, 55], Erlang [49], F\(\sharp \) [48], Go [11, 37, 38, 51], Java [30, 31, 34, 65], OCaml [56], C [52], Python [16, 47, 50], Rust [32], and Scala [61, 62]. Communicating automata and asynchronous multiparty session types [28] are closely related: the latter can be seen as a syntactical representation of the former [17] where a sending state corresponds to an internal choice and a receiving state to an external choice. This correspondence between communicating automata and multiparty session types has become the foundation of many tools centred on session types, e.g., for generating communication API from multiparty session (global) types [30, 31, 48, 61], for detecting deadlocks in messagepassing programs [51, 67], and for monitoring sessionenabled programs [5, 16, 47, 49, 50]. These tools rely on a property called multiparty compatibility [6, 18, 39], which guarantees that communicating automata representing session types interact correctly, hence enabling the identification of correct protocols or the detection of errors in endpoint programs. Multiparty compatible communicating automata validate two essential requirements for session types frameworks: every message that is sent can be eventually received and each automaton can always eventually make a move. Thus, they satisfy the abstract safety invariant \({\varphi }\) for session types from [63], a prerequisite for session type systems to guarantee safety of the typed processes. Unfortunately, multiparty compatibility suffers from a severe limitation: it requires that each execution of the system has a synchronous equivalent. Hence, it rules out many correct systems. Hereafter, we refer to this property as synchronous multiparty compatibility (smc) and explain its main limitation with Example 1.
Example 1
The system in Fig. 1 contains an interaction pattern that is not supported by any definition of smc [6, 18, 39]. It consists of a client (\({\mathtt{c}}\)), a server (\({\mathtt{s}}\)), and a logger (\({\mathtt{l}}\)), which communicate via unbounded fifo channels. Transition \({\mathtt{sr}} ! a \) denotes that \({\mathtt{s}}\)ender puts (asynchronously) message \( a \) on channel \({\mathtt{sr}}\); and transition \({\mathtt{sr}} ? a \) denotes the consumption of \( a \) from channel \({\mathtt{sr}}\) by \({\mathtt{r}}\)eceiver. The \({\mathtt{c}}\)lient sends a \( req \)uest and some \( data \) in a fireandforget fashion, before waiting for a response from the \({\mathtt{s}}\)erver. Because of the presence of this simple pattern, the system cannot be executed synchronously (i.e., with the restriction that a send action can only be fired when a matching receive is enabled), hence it is rejected by all definitions of smc from previous works, even though the system is safe (all sent messages are received and no automaton gets stuck).
Synchronous multiparty compatibility is reminiscent of a strong form of existential boundedness. Among the existing subclasses of communicating automata (see [46] for a survey), existentially kbounded communicating automata [22] stand out because they can be modelchecked [8, 21] and they restrict the model in a natural way: any execution can be rescheduled such that the number of pending messages that can be received is bounded by k. However, existential boundedness is generally undecidable [22], even for a fixed bound k. This shortcoming makes it impossible to know when theoretical results are applicable.
To address the limitation of smc and the shortcoming of existential boundedness, we propose a (decidable) sufficient condition for existential boundedness, called kexhaustivity, which serves as a basis for a wider notion of new compatibility, called kmultiparty compatibility (kmc) where \(k \in \mathbb {N}_{>0}\) is a bound on the number of pending messages in each channel. A system is kmc when it is (i) kexhaustive, i.e., all kreachable send actions are enabled within the bound, and (ii) ksafe, i.e., within the bound k, all sent messages can be received and each automaton can always eventually progress. For example, the system in Fig. 1 is kmultiparty compatible for any \(k \in \mathbb {N}_{>0}\), hence it does not lead to communication errors, see Theorem 1. The kmc condition is a natural constraint for realworld systems. Indeed any finitestate system is kexhaustive (for k sufficiently large), while any system that is not kexhaustive (resp. ksafe) for any k is unlikely to work correctly. Furthermore, we show that if a system of csa validates kexhaustivity, then each automaton locally behaves equivalently under any bound greater than or equal to k, a property that we call local boundagnosticity. We give a sound and complete characterisation of kexhaustivity for csa in terms of local boundagnosticity, see Theorem 3. Additionally, we show that the complexity of checking kmc is pspacecomplete (i.e., no higher than related algorithms) and we demonstrate empirically that its cost can be mitigated through (sound and complete) partial order reduction.
In this paper, we consider communicating session automata (csa), which cover the most common form of asynchronous multiparty session types [15] (see Remark 3), and have been used as a basis to study properties and extensions of session types [6, 7, 18, 30, 31, 41, 42, 47, 49, 50]. More precisely, csa are deterministic automata, whose every state is either sending (internal choice), receiving (external choice), or final. We focus on csa that preserve the intent of internal and external choices from session types. In these csa, whenever an automaton is in a sending state, it can fire any transition, no matter whether channels are bounded; when it is in a receiving state then at most one action must be enabled.
Synopsis. In Sect. 2, we give the necessary background on communicating automata and their properties, and introduce the notions of output/input bound independence which guarantee that internal/external choices are preserved in bounded semantics. In Sect. 3, we introduce the definition of kmultiparty compatibility (kmc) and show that kmc systems are safe for systems which validate the bound independence properties. In Sect. 4, we formally relate existential boundedness [22, 35], synchronisability [9], and kexhaustivity. In Sect. 5 we present an implementation (using partial order reduction) and an experimental evaluation of our theory. We discuss related works in Sect. 6 and conclude in Sect. 7.
2 Communicating Automata and Bound Independence
This section introduces notations and definitions of communicating automata (following [12, 39]), as well as the notion of output (resp. input) bound independence which enforces the intent of internal (resp. external) choice in csa.
Fix a finite set \(\mathcal {P}\) of participants (ranged over by \({\mathtt{p}}\), \({\mathtt{q}}\), \({\mathtt{r}}\), \({\mathtt{s}}\), etc.) and a finite alphabet \(\varSigma \). The set of channels is Open image in new window , Open image in new window is the set of actions (ranged over by \(\ell \)), \(\varSigma ^{*}\) (resp. \(\mathcal {A}^*\)) is the set of finite words on \(\varSigma \) (resp. \(\mathcal {A}\)). Let \(w\) range over \(\varSigma ^{*}\), and \(\phi , \psi \) range over \(\mathcal {A}^*\). Also, \(\epsilon \) (\(\notin \varSigma \cup \mathcal {A}\)) is the empty word, \(w\) denotes the length of \(w\), and Open image in new window is the concatenation of \(w\) and \(w'\) (these notations are overloaded for words in \(\mathcal {A}^*\)).
Definition 1
(Communicating automaton). A communicating automaton is a finite transition system given by a triple \(M = (Q,q_0,\delta )\) where Q is a finite set of states, \(q_0\in Q\) is the initial state, and \(\delta \ \subseteq \ Q \times \mathcal {A}\times Q\) is a set of transitions.
The transitions of a communicating automaton are labelled by actions in \(\mathcal {A}\) of the form \({\mathtt{sr}} ! a \), representing the emission of message a from participant \({\mathtt{s}}\) to \({\mathtt{r}}\), or \({\mathtt{sr}} ? a \) representing the reception of a by \({\mathtt{r}}\). Define \( subj ({\mathtt{pq}} ! a ) = subj ({\mathtt{qp}} ? a ) = {\mathtt{p}}\), \( obj ({\mathtt{pq}} ! a ) = obj ({\mathtt{qp}} ? a ) = {\mathtt{q}}\), and \( chan ({\mathtt{pq}} ! a ) = chan ({\mathtt{pq}} ? a ) = {\mathtt{pq}}\). The projection of \(\ell \) onto \({\mathtt{p}}\) is defined as \(\pi _{{\mathtt{p}}}^{}(\ell ) = \ell \) if \( subj (\ell ) = {\mathtt{p}}\) and \(\pi _{{\mathtt{p}}}^{}(\ell ) = \epsilon \) otherwise. Let \(\dagger \) range over \(\{!,?\}\), we define: \(\pi _{{\mathtt{pq}}}^{\dagger }({\mathtt{pq}} \dagger a ) = a \) and \(\pi _{{\mathtt{pq}}}^{\dagger '}({\mathtt{sr}} \dagger a )=\epsilon \) if either \({\mathtt{pq}} \ne {\mathtt{sr}}\) or \(\dagger \ne \dagger '\). We extend these definitions to sequences of actions in the natural way.
A state \(q\in Q\) with no outgoing transition is final; q is sending (resp. receiving) if it is not final and all its outgoing transitions are labelled by send (resp. receive) actions, and q is mixed otherwise. \(M=(Q, q_{0},\delta )\) is deterministic if Open image in new window . \(M=(Q, q_{0},\delta )\) is send (resp. receive) directed if for all sending (resp. receiving) \(q \in Q\) and \((q,\ell ,q'), (q,\ell ',q'') \in \delta : obj (\ell ) = obj (\ell ')\). M is directed if it is send and receive directed.
Remark 1
In this paper, we consider only deterministic communicating automata without mixed states, and call them Communicating Session Automata (csa). We discuss possible extensions of our results beyond this class in Sect. 7.
Definition 2
(System). Given a communicating automaton \(M_{\mathtt{p}}=(Q_{\mathtt{p}}, q_{0{\mathtt{p}}},\delta _{\mathtt{p}})\) for each \({\mathtt{p}}\in \mathcal {P}\), the tuple \(S=(M_{\mathtt{p}})_{{\mathtt{p}}\in \mathcal {P}}\) is a system. A configuration of S is a pair \(s = (\varvec{q}; \varvec{w})\) where \(\varvec{q}=(q_{\mathtt{p}})_{{\mathtt{p}}\in \mathcal {P}}\) with \(q_{\mathtt{p}}\in Q_{\mathtt{p}}\) and where \(\varvec{w}=(w_{{\mathtt{p}}{\mathtt{q}}})_{{\mathtt{p}}{\mathtt{q}}\in \mathcal {C}}\) with \(w_{{\mathtt{p}}{\mathtt{q}}}\in \varSigma ^*\); component \(\varvec{q}\) is the control state and \(q_{\mathtt{p}}\in Q_{\mathtt{p}}\) is the local state of automaton \(M_{\mathtt{p}}\). The initial configuration of S is \(s_0 = (\varvec{q_0}; \varvec{\epsilon })\) where \(\varvec{q_0} = (q_{0{\mathtt{p}}})_{{\mathtt{p}}\in \mathcal {P}}\) and we write \({\varvec{\epsilon }}\) for the \(\mathcal {C}\)tuple \((\epsilon , \ldots , \epsilon )\).
Hereafter, we fix a communicating session automaton \(M_{\mathtt{p}}=(Q_{\mathtt{p}}, q_{0{\mathtt{p}}},\delta _{\mathtt{p}})\) for each \({\mathtt{p}}\in \mathcal {P}\) and let \(S=(M_{\mathtt{p}})_{{\mathtt{p}}\in \mathcal {P}}\) be the corresponding system whose initial configuration is \(s_0\). For each \({\mathtt{p}}\in \mathcal {P}\), we assume that \(\forall (q,\ell ,q') \in \delta _{\mathtt{p}}: subj (\ell ) = {\mathtt{p}}\). We assume that the components of a configuration are named consistently, e.g., for \(s' = (\varvec{q'}; \varvec{w'})\), we implicitly assume that \(\varvec{q'}=(q'_{\mathtt{p}})_{{\mathtt{p}}\in \mathcal {P}}\) and \(\varvec{w'}=(w'_{{\mathtt{p}}{\mathtt{q}}})_{{\mathtt{p}}{\mathtt{q}}\in \mathcal {C}}\).
Definition 3
 1.
(a) \(\ell = {\mathtt{sr}} ! a \) and \((q_{\mathtt{s}},\ell ,q_{\mathtt{s}}') \in \delta _{{\mathtt{s}}}\), (b) \(q_{{\mathtt{p}}}' = q_{{\mathtt{p}}}\) for all \({{\mathtt{p}}} \ne {\mathtt{s}}\), (c) Open image in new window and \(w_{{\mathtt{p}}{\mathtt{q}}}'=w_{{\mathtt{p}}{\mathtt{q}}}\) for all \({{\mathtt{p}}{\mathtt{q}}} \ne {\mathtt{s}}{\mathtt{r}}\); or
 2.
(a) \(\ell = {\mathtt{sr}} ? a \) and \((q_{\mathtt{r}},\ell ,q_{\mathtt{r}}')\in \delta _{\mathtt{r}}\), (b) \(q_{{\mathtt{p}}}' = q_{{\mathtt{p}}}\) for all \({{\mathtt{p}}} \ne {\mathtt{r}}\), (c) Open image in new window , and \(w_{{\mathtt{p}}{\mathtt{q}}}'=w_{{\mathtt{p}}{\mathtt{q}}}\) for all \({{\mathtt{p}}{\mathtt{q}}} \ne {\mathtt{sr}}\).
Remark 2
Hereafter, we assume that any bound k is finite and \(k \in \mathbb {N}_{>0}\).
We write \(\xrightarrow {}\negthickspace ^*\) for the reflexive and transitive closure of \(\xrightarrow {}\). Configuration \((\varvec{q}; \varvec{w})\) is kbounded if \(\forall {\mathtt{pq}} \in \mathcal {C}:w_{{\mathtt{p}}{\mathtt{q}}} \le k\). We write \(s_1 \xrightarrow {\ell _1\cdots \ell _n} s_{n+1}\) when \(s_1 \xrightarrow {\ell _1} s_2 \cdots s_n \xrightarrow {\ell _n} s_{n+1}\), for some \(s_2,\ldots ,s_n\) (with \(n \ge 0\)); and say that the execution \(\ell _1\cdots \ell _n\) is kbounded from \(s_1\) if \(\forall 1 \le i \le n{+}1 :s_i\) is kbounded. Given \(\phi \in \mathcal {A}^*\), we write \({\mathtt{p}}\notin \phi \) iff Open image in new window . We write \(s \xrightarrow {\phi }_{k} s'\) if \(s'\) is reachable with a kbounded execution \(\phi \) from s. The set of reachable configurations of S is \( RS (S)=\{ s \, \mid \,s_0 \xrightarrow {}\negthickspace ^*s\}\). The kreachability set of S is the largest subset \( RS _k(S)\) of \( RS (S)\) within which each configuration s can be reached by a kbounded execution from \(s_0\).
Definition 4 streamlines notions of safety from previous works [6, 12, 18, 39] (absence of deadlocks, orphan messages, and unspecified receptions).
Definition 4

( er) \(\forall {\mathtt{p}}{\mathtt{q}}\in \mathcal {C}\), if \(w_{{\mathtt{p}}{\mathtt{q}}} = a \cdot w'\), then \((\varvec{q}; \varvec{w}) \xrightarrow {}_{k}\negthickspace ^*\xrightarrow {{\mathtt{pq}} ? a }_{k}\).

( pg) \(\forall {\mathtt{p}}\in \mathcal {P}\), if \(q_{\mathtt{p}}\) is receiving, then \((\varvec{q}; \varvec{w}) \xrightarrow {}_{k}\negthickspace ^*\xrightarrow {{\mathtt{qp}} ? a }_{k}\) for \({\mathtt{q}}\in \mathcal {P}\) and \( a \in \varSigma \).
We say that S is safe if it validates the unbounded version of ksafety (\(\infty \)safe).
Property (er), called eventual reception, requires that any sent message can always eventually be received (i.e., if \( a \) is the head of a queue then there must be an execution that consumes \( a \)), and Property (pg), called progress, requires that any automaton in a receiving state can eventually make a move (i.e., it can always eventually receive an expected message).
We say that a configuration s is stable iff \(s = (\varvec{q}; \varvec{\epsilon })\), i.e., all its queues are empty. Next, we define the stable property for systems of communicating automata, following the definition from [18].
Definition 5
(Stable). S has the stable property (sp) if \(\forall s \in RS (S) :\exists (\varvec{q}; \varvec{\epsilon }) \in RS (S) :s \xrightarrow {}\negthickspace ^*(\varvec{q}; \varvec{\epsilon })\).
A system has the stable property if it is possible to reach a stable configuration from any reachable configuration. This property is called deadlockfree in [22]. The stable property implies the eventual reception property, but not safety (e.g., an automaton may be waiting for an input in a stable configuration, see Example 2), and safety does not imply the stable property, see Example 4.
Example 2
Next, we define two properties related to bound independence. They specify classes of csa whose branching behaviours are not affected by channel bounds.
Definition 6
(kobi). S is koutput bound independent (\({k}\text {}\textsc {obi}\)), if \(\forall s = (\varvec{q}; \varvec{w}) \in RS _k(S)\) and \(\forall {\mathtt{p}}\in \mathcal {P}\), if \(s \xrightarrow {{\mathtt{pq}} ! a }_{k}\), then \(\forall (q_{\mathtt{p}}, {\mathtt{pr}} ! b , q'_{\mathtt{p}}) \in \delta _{\mathtt{p}}:s\xrightarrow {{\mathtt{pr}} ! b }_{k}\).
Definition 7
(kibi). S is kinput bound independent (\({k}\text {}\textsc {ibi}\)), if \(\forall s = (\varvec{q}; \varvec{w}) \in RS _k(S)\) and \(\forall {\mathtt{p}}\in \mathcal {P}\), if \(s \xrightarrow {{\mathtt{qp}} ? a }_{k}\), then Open image in new window .
If S is \({k}\text {}\textsc {obi}\), then any automaton that reaches a sending state is able to fire any of its available transitions, i.e., sending states model internal choices which are not constrained by bounds greater than or equal to k. Note that the unbounded version of \({k}\text {}\textsc {obi}\) (\(k=\infty \)) is trivially satisfied for any system due to unbounded asynchrony. If S is \({k}\text {}\textsc {ibi}\), then any automaton that reaches a receiving state is able to fire at most one transition, i.e., receiving states model external choices where the behaviour of the receiving automaton is controlled exclusively by its environment. We write \(\textsc {ibi}\) for the unbounded version of \({k}\text {}\textsc {ibi}\) (\(k = \infty \)).
Checking the \(\textsc {ibi}\) property is generally undecidable. However, systems consisting of (send and receive) directed automata are trivially \({k}\text {}\textsc {ibi}\) and \({k}\text {}\textsc {obi}\) for all k, this subclass of csa was referred to as basic in [18]. We introduce larger decidable approximations of \(\textsc {ibi}\) with Definitions 10 and 11.
Proposition 1
(1) If S is send directed, then S is \({k}\text {}\textsc {obi}\) for all \(k \in \mathbb {N}_{>0}\). (2) If S is receive directed, then S is \(\textsc {ibi}\) (and \({k}\text {}\textsc {ibi}\) for all \(k \in \mathbb {N}_{>0}\)).
Remark 3
csa validating \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\) strictly include the most common forms of asynchronous multiparty session types, e.g., the directed csa of [18], and systems obtained by projecting Scribble specifications (global types) which need to be receive directed (this is called “consistent external choice subjects” in [31]) and which validate \({1}\text {}\textsc {obi}\) by construction since they are projections of synchronous specifications where choices must be located at a unique sender.
3 Bounded Compatibility for csa
In this section, we introduce kmultiparty compatibility (kmc) and study its properties wrt. Safety of communicating session automata (csa) which are \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\). Then, we soundly and completely characterise kexhaustivity in terms of local boundagnosticity, a property which guarantees that communicating automata behave equivalently under any bound greater than or equal to k.
3.1 Multiparty Compatibility
Definition 8
(kExhaustivity). S is kexhaustive if \(\forall (\varvec{q}; \varvec{w}) \in RS _k(S)\) and \(\forall {\mathtt{p}}\in \mathcal {P}\), if \(q_{\mathtt{p}}\) is sending, then \(\forall (q_{\mathtt{p}}, \ell , q'_{\mathtt{p}}) \in \delta _{\mathtt{p}}:\exists \phi \in \mathcal {A}^*:(\varvec{q}; \varvec{w}) \xrightarrow {\phi }_{k}\xrightarrow {\ell }_{k} \wedge {\mathtt{p}}\notin \phi .\)
Definition 9
(kMultiparty compatibility). S is kmultiparty compatible (kmc) if it is ksafe and kexhaustive.
Definition 9 is a natural extension of the definitions of synchronous multiparty compatibility given in [18, Definition 4.2] and [6, Definition 4]. The common key requirements are that every send action must be matched by a receive action (i.e., send actions are universally quantified), while at least one receive action must find a matching send action (i.e., receive actions are existentially quantified). Here, the universal check on send actions is done via the eventual reception property (er) and the kexhaustivity condition; while the existential check on receive actions is dealt with by the progress property (pg).
Whenever systems are \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\), then kexhaustivity implies that kbounded executions are sufficient to make a sound decision wrt. safety. This is not necessarily the case for systems outside of this class, see Examples 3 and 5.
Example 3
The system \((M_{\mathtt{p}},M_{\mathtt{q}},M_{\mathtt{r}})\) in Fig. 2 is \({k}\text {}\textsc {obi}\) for any k, but not ibi (it is \({1}\text {}\textsc {ibi}\) but not \({k}\text {}\textsc {ibi}\) for any \(k \ge 2\)). When executing with a bound strictly greater than 1, there is a configuration where \(M_{\mathtt{q}}\) is in its initial state and both its receive transitions are enabled. The system is 1safe and 1exhaustive (hence 1mc) but it is not 2exhaustive nor 2safe. By constraining the automata to execute with a channel bound of 1, the left branch of \(M_{\mathtt{p}}\) is prevented to execute together with the right branch of \(M_{\mathtt{q}}\). Thus, the fact that the \( y \) messages are not received in this case remains invisible in 1bounded executions. This example can be easily extended so that it is nexhaustive (resp. safe) but not \(n{+1}\)exhaustive (resp. safe) by sending/receiving \(n{+}1\) \( a_i \) messages.
Example 4
The system in Fig. 1 is directed and 1mc. The system \((M_{\mathtt{p}}, M_{\mathtt{q}})\) in Fig. 3 is safe but not kmc for any finite \(k \in \mathbb {N}_{>0}\). Indeed, for any execution of this system, at least one of the queues grows arbitrarily large. The system \((M_{\mathtt{p}}, N_{\mathtt{q}})\) is 1mc while the system \((M_{\mathtt{p}}, N'_{\mathtt{q}})\) is not 1mc but it is 2mc.
Example 5
The system in Fig. 4 (without the dotted transition) is 1mc, but not 2safe; it is not \({1}\text {}\textsc {obi}\) but it is \({2}\text {}\textsc {obi}\). In 1bounded executions, \(M_{\mathtt{r}}\) can execute Open image in new window , but it cannot fire Open image in new window (queue \({\mathtt{rs}}\) is full), which violates the \({1}\text {}\textsc {obi}\) property. The system with the dotted transition is not \({1}\text {}\textsc {obi}\), but it is \({2}\text {}\textsc {obi}\) and kmc for any \(k \ge 1\). Both systems are receive directed, hence \(\textsc {ibi}\).
Theorem 1
If S is \({k}\text {}\textsc {obi}\), \(\textsc {ibi}\), and kmc, then it is safe.
Remark 4
It is undecidable whether there exists a bound k for which an arbitrary system is kmc. This is a consequence of the Turing completeness of communicating (session) automata [10, 20, 42].
Definition 10
S is kchained input bound independent (\({k}{\text {}\textsc {cibi}}\)) if \(\forall s = (\varvec{q}; \varvec{w}) \in RS _k(S)\) and \(\forall {\mathtt{p}}\in \mathcal {P}\), if \(s \xrightarrow {{\mathtt{qp}} ? a }_{k} s'\), then \(\forall (q_{\mathtt{p}}, {\mathtt{sp}} ? b , q'_{\mathtt{p}}) \in \delta _{\mathtt{p}}:{\mathtt{s}}\ne {\mathtt{q}}\implies \! \lnot ( s \xrightarrow {{\mathtt{sp}} ? b }_{k}) \wedge ( \forall \phi \in \mathcal {A}^*:s' \xrightarrow {\phi }_{k} \xrightarrow {{\mathtt{sp}} ! b }_{k} \implies s \vdash {\mathtt{qp}} ? a \prec _{\phi } {\mathtt{sp}} ! b )\).
Definition 11
S is kstrong input bound independent (\({k}\text {}\textsc {sibi}\)) if \(\forall s = (\varvec{q}; \varvec{w}) \in RS _k(S)\) and \(\forall {\mathtt{p}}\in \mathcal {P}\), if \(s \xrightarrow {{\mathtt{qp}} ? a }_{k} s'\), then \(\forall (q_{\mathtt{p}}, {\mathtt{sp}} ? b , q'_{\mathtt{p}}) \in \delta _{\mathtt{p}}:{\mathtt{s}}\ne {\mathtt{q}}\implies \! \lnot ( s \xrightarrow {{\mathtt{sp}} ? b }_{k} \, \vee \, s' \xrightarrow {}_{k}\negthickspace ^*\xrightarrow {{\mathtt{sp}} ! b }_{k})\).
Definition 10 requires that whenever \({\mathtt{p}}\) can fire a receive action, at most one of its receive actions is enabled at s, and no other receive transition from \(q_{\mathtt{p}}\) will be enabled until \({\mathtt{p}}\) has made a move. This is due to the existence of a dependency chain between the reception of a message (\({{\mathtt{qp}} ? a }\)) and the matching send of another possible reception (\({{\mathtt{sp}} ! b }\)). Property \({k}\text {}\textsc {sibi}\) (Definition 11) is a stronger version of \({k}{\text {}\textsc {cibi}}\), which can be checked more efficiently.
Lemma 1
If S is \({k}\text {}\textsc {obi}\), \({k}{\text {}\textsc {cibi}}\) (resp. \({k}\text {}\textsc {sibi}\)) and kexhaustive, then it is \(\textsc {ibi}\).
The decidability of \({k}\text {}\textsc {obi}\), \({k}\text {}\textsc {ibi}\), \({k}\text {}\textsc {sibi}\), \({k}{\text {}\textsc {cibi}}\), and kmc is straightforward since both \( RS _k(S)\) (which has an exponential number of states wrt. k) and \(\xrightarrow {}_{k}\) are finite, given a finite k. Theorem 2 states the space complexity of the procedures, except for \({k}{\text {}\textsc {cibi}}\) for which a complexity class is yet to be determined. We show that the properties are pspace by reducing to an instance of the reachability problem over a transition system built following the construction of Bollig et al. [8, Theorem 6.3]. The rest of the proof follows from similar arguments in Genest et al. [22, Proposition 5.5] and Bouajjani et al. [9, Theorem 3].
Theorem 2
The problems of checking the \({k}\text {}\textsc {obi}\), \({k}\text {}\textsc {ibi}\), \({k}\text {}\textsc {sibi}\), ksafety, and kexhaustivity properties are all decidable and pspacecomplete (with \(k \in \mathbb {N}_{>0}\) given in unary). The problem of checking the \({k}{\text {}\textsc {cibi}}\) property is decidable.
3.2 Local BoundAgnosticity
We introduce local boundagnosticity and show that it fully characterises kexhaustive systems. Local boundagnosticity guarantees that each communicating automaton behave in the same manner for any bound greater than or equal to some k. Therefore such systems may be executed transparently under a bounded semantics (a communication model available in Go and Rust).
Definition 12
(Transition system). The kbounded transition system of S is the labelled transition system (LTS) \( TS _{k}(S) = (N, s_0, \varDelta )\) such that \(N = RS _k(S)\), \(s_0\) is the initial configuration of S, \(\varDelta \subseteq N {\times } \mathcal {A}{\times } N\) is the transition relation, and \((s, \ell , s') \in \varDelta \) if and only if \(s \xrightarrow {\ell }_{k} s'\).
Definition 13
(Projection). Let \(\mathcal {T}\) be an LTS over \(\mathcal {A}\). The projection of \(\mathcal {T}\) onto \({\mathtt{p}}\), written \(\pi _{{\mathtt{p}}}^{\epsilon }(\mathcal {T})\), is obtained by replacing each label \(\ell \) in \(\mathcal {T}\) by \(\pi _{{\mathtt{p}}}^{}(\ell )\).
Recall that the projection of action \(\ell \), written \(\pi _{{\mathtt{p}}}^{}(\ell )\), is defined in Sect. 2. The automaton \(\pi _{{\mathtt{p}}}^{\epsilon }( TS _{k}(S))\) is essentially the local behaviour of participant \({\mathtt{p}}\) within the transition system \( TS _{k}(S)\). When each automaton in a system S behaves equivalently for any bound greater than or equal to some k, we say that S is locally boundagnostic. Formally, S is locally boundagnostic for k when \(\pi _{{\mathtt{p}}}^{\epsilon }( TS _{k}(S))\) and \(\pi _{{\mathtt{p}}}^{\epsilon }( TS _{n}(S))\) are weakly bisimilar ( Open image in new window ) for each participant \({\mathtt{p}}\) and any \(n \ge k\). For \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\) systems, local boundagnosticity is a necessary and sufficient condition for kexhaustivity, as stated in Theorem 3 and Corollary 1.
Theorem 3
Let S be a system.
 (1)
If Open image in new window , then S is kexhaustive.
 (2)
If S is \({k}\text {}\textsc {obi}\), \(\textsc {ibi}\), and kexhaustive, then Open image in new window .
Corollary 1
Let S be \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\) s.t. Open image in new window , then S is locally boundagnostic for k.
4 Existentially Bounded and Synchronisable Automata
4.1 Kuske and Muscholl’s Existential Boundedness
Existentially bounded communicating automata [21, 22, 35] are a class of communicating automata whose executions can always be scheduled in such a way that the number of pending messages is bounded by a given value. Traditionally, existentially bounded communicating automata are defined on communicating automata that feature (local) accepting states and in terms of accepting runs. An accepting run is an execution (starting from \(s_0\)) which terminates in a configuration \((\varvec{q}; \varvec{w})\) where each \(q_{\mathtt{p}}\) is a local accepting state. In our setting, we simply consider that every local state \(q_{\mathtt{p}}\) is an accepting state, hence any execution \(\phi \) starting from \(s_0\) is an accepting run. We first study existential boundedness as defined in [35] as it matches more closely kexhaustivity, we study the “classical” definition of existential boundedness [22] in Sect. 4.2.
Following [35], we say that an execution \(\phi \in \mathcal {A}^*\) is valid if for any prefix \(\psi \) of \(\phi \) and any channel \({\mathtt{pq}} \in \mathcal {C}\), we have that \(\pi _{{\mathtt{pq}}}^{?}(\psi )\) is a prefix of \(\pi _{{\mathtt{pq}}}^{!}(\psi )\), i.e., an execution is valid if it models the fifo semantics of communicating automata.
Definition 14
(Causal equivalence [35]). Given \(\phi , \psi \in \mathcal {A}^*\), we define: Open image in new window iff \(\phi \) and \(\psi \) are valid executions and \(\forall {\mathtt{p}}\in \mathcal {P}:\pi _{{\mathtt{p}}}^{}(\phi ) = \pi _{{\mathtt{p}}}^{}(\psi )\). We write Open image in new window for the equivalence class of \(\phi \) wrt. Open image in new window .
Definition 15
(Existential boundedness [35]). We say that a valid execution \(\phi \) is kmatchbounded if, for every prefix \(\psi \) of \(\phi \) the difference between the number of matched events of type \({\mathtt{pq}} ! \) and those of type \({\mathtt{pq}} ? \) is bounded by k, i.e., \( min \{ \pi _{{\mathtt{pq}}}^{!}(\psi ) , \pi _{{\mathtt{pq}}}^{?}(\phi ) \}  \pi _{{\mathtt{pq}}}^{?}(\psi ) \le k\).
Write \(\mathcal {A}^* \!\! \mid _{k}\) for the set of kmatchbounded words. An execution \(\phi \) is existentially kbounded if Open image in new window . A system S is existentially kbounded, written \(\exists \)kbounded, if each execution in \(\{\phi \, \mid \,\exists s :s_0 \smash {\xrightarrow {\phi }} s \}\) is existentially kbounded.
Example 6
Consider Fig. 3. \((M_{\mathtt{p}}, M_{\mathtt{q}})\) is not existentially kbounded, for any k: at least one of the queues must grow infinitely for the system to progress. Systems \((M_{\mathtt{p}}, N_{\mathtt{q}})\) and \((M_{\mathtt{p}}, N'_{\mathtt{q}})\) are existentially bounded since any of their executions can be scheduled to an Open image in new window equivalent execution which is 2matchbounded.
The relationship between kexhaustivity and existential boundedness is stated in Theorem 4 and illustrated in Fig. 5 for \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\) csa, where smc refers to synchronous multiparty compatibility [18, Definition 4.2]. The circled numbers in the figure refer to key examples summarised in Table 1. The strict inclusion of kexhaustivity in existential kboundedness is due to systems that do not have the eventual reception property, see Example 7.
Example 7
For any k, the channel \({\mathtt{sp}}\) eventually gets full and the send action \({\mathtt{sp}} ! b \) can no longer be fired; hence it does not satisfy kexhaustivity. Note that each execution can be reordered into a 1matchbounded execution (the \( b \)’s are never matched).
Theorem 4
(1) If S is \({k}\text {}\textsc {obi}\), \(\textsc {ibi}\), and kexhaustive, then it is \(\exists \)kbounded. (2) If S is \(\exists \)kbounded and satisfies eventual reception, then it is kexhaustive.
4.2 Existentially Stable Bounded Communicating Automata
The “classical” definition of existentially bounded communicating automata as found in [22] differs slightly from Definition 15, as it relies on a different notion of accepting runs, see [22, page 4]. Assuming that all local states are accepting, we adapt their definition as follows: a stable accepting run is an execution \(\phi \) starting from \(s_0\) which terminates in a stable configuration.
Definition 16
(Existential stable boundedness [22]). A system S is existentially stable kbounded, written \(\exists \)Skbounded, if for each execution \(\phi \) in \(\{\phi \, \mid \,\exists (\varvec{q}; \varvec{\epsilon }) \in RS (S) :s_0 \xrightarrow {\phi } (\varvec{q}; \varvec{\epsilon }) \}\) there is \(\psi \) such that \(s_0 \xrightarrow {\psi }_{k}\) with Open image in new window .
A system is existentially stable kbounded if each of its executions leading to a stable configuration can be reordered into a kbounded execution (from \(s_0\)).
Theorem 5
(1) If S is existentially kbounded, then it is existentially stable kbounded. (2) If S is existentially stable kbounded and has the stable property, then it is existentially kbounded.
We illustrate the relationship between existentially stable bounded communicating automata and the other classes in Fig. 5. The example below further illustrates the strictness of the inclusions, see Table 1 for a summary.
Example 8
Consider the systems in Fig. 3. \((M_{\mathtt{p}}, M_{\mathtt{q}})\) and \((M_{\mathtt{p}}, N'_{\mathtt{q}})\) are (trivially) existentially stable 1bounded since none of their (nonempty) executions terminate in a stable configuration. The system \((M_{\mathtt{p}}, N_{\mathtt{q}})\) is existentially stable 2bounded since each of its executions can be reordered into a 2bounded one. The system in Example 7 is (trivially) \(\exists \)S1bounded: none of its (nonempty) executions terminate in a stable configuration (the \( b \)’s are never received).
Theorem 6
Let S be an \(\exists \)(S)kbounded system with the stable property, then it is kexhaustive.
Properties for key examples, where direct. stands for directed, \(\textsc {obi}\) for \({k}\text {}\textsc {obi}\), \(\textsc {sibi}\) for \({k}\text {}\textsc {sibi}\), er for eventual reception property, sp for stable property, exh. for kexhaustive, \(\exists \)(S)b for \(\exists \)(S)bounded, and syn. for nsynchronisable (for some \(n \in \mathbb {N}_{>0}\)).
#  System  Ref.  k  direct.  \(\textsc {obi}\)  \(\textsc {sibi}\)  safe  er  sp  exh.  \(\exists \)Sb  \(\exists \)b  syn. 

1  \((M_{\mathtt{c}},M_{\mathtt{s}},M_{\mathtt{l}}) \)  Figure 1  1  yes  yes  yes  yes  yes  yes  yes  yes  yes  yes 
2  \((M_{\mathtt{s}},M_{\mathtt{q}},M_{\mathtt{r}})\)  Example 2  1  yes  yes  yes  no  yes  yes  yes  yes  yes  yes 
3  \((M_{\mathtt{p}},M_{\mathtt{q}},M_{\mathtt{r}}) \)  Figure 2  \(\ge 2\)  no  yes  no  no  no  no  no  yes  yes  no 
4  \((M_{\mathtt{p}},M_{\mathtt{q}}) \)  Figure 3  any  yes  yes  yes  yes  yes  no  no  yes  no  no 
5  \((M_{\mathtt{p}},N'_{\mathtt{q}}) \)  Figure 3  2  yes  yes  yes  yes  yes  no  yes  yes  yes  no 
6  \((M_{\mathtt{p}},M_{\mathtt{q}},M_{\mathtt{r}},M_{\mathtt{s}}) \)  Figure 4  2  no  yes  yes  yes  yes  no  yes  yes  yes  no 
7  \((M_{\mathtt{s}},M_{\mathtt{r}},M_{\mathtt{p}}) \)  Example 7  any  yes  yes  yes  no  no  no  no  yes  yes  yes 
8  \((M_{\mathtt{p}},M_{\mathtt{q}}) \)  Example 9  1  yes  yes  yes  yes  yes  yes  yes  yes  yes  no 
Experimental evaluation. \(\mathcal {P}\) is the number of participants, k is the bound, \( RTS \) is the number of transitions in the reduced \( TS _{k}(S)\) (see [43]), direct. stands for directed, Time is the time taken to check all the properties shown in this table, and gmc is yes if the system is generalised multiparty compatible [39].
Example  \(\mathcal {P}\)  k  \( RTS \)  direct.  \({k}\text {}\textsc {obi}\)  \({k}{\text {}\textsc {cibi}}\)  kmc  Time  gmc 

ClientServerLogger  3  1  11  yes  yes  yes  yes  0.04 s  no 
4 Player game Open image in new window [39]  4  1  20  no  yes  yes  yes  0.05 s  yes 
Bargain [39]  3  1  8  yes  yes  yes  yes  0.03 s  yes 
Filter collaboration [68]  2  1  10  yes  yes  yes  yes  0.03 s  yes 
Alternating bit Open image in new window [59]  2  1  8  yes  yes  yes  yes  0.04 s  no 
TPMContract v2 Open image in new window [25]  2  1  14  yes  yes  yes  yes  0.04 s  yes 
Sanitary agency Open image in new window [60]  4  1  34  yes  yes  yes  yes  0.07 s  yes 
Logistic Open image in new window [54]  4  1  26  yes  yes  yes  yes  0.05 s  yes 
Cloud system v4 [24]  4  2  16  no  yes  yes  yes  0.04 s  yes 
Commit protocol [9]  4  1  12  yes  yes  yes  yes  0.03 s  yes 
Elevator Open image in new window [9]  5  1  72  no  yes  no  yes  0.14s  no 
Elevatordashed Open image in new window [9]  5  1  80  no  yes  no  yes  0.16s  no 
Elevatordirected Open image in new window [9]  3  1  41  yes  yes  yes  yes  0.07 s  yes 
Dev system [58]  4  1  20  yes  yes  yes  yes  0.05 s  no 
Fibonacci [48]  2  1  6  yes  yes  yes  yes  0.03 s  yes 
2  1  18  yes  yes  yes  yes  0.04 s  yes  
sh [48]  3  1  30  yes  yes  yes  yes  0.06 s  yes 
3  1  21  yes  yes  yes  yes  0.05 s  yes  
2  1  48  yes  yes  yes  yes  0.07 s  yes  
2  1  108  yes  yes  yes  yes  0.08 s  yes  
gen_server (buggy) [67]  3  1  56  no  no  yes  no  0.03 s  no 
gen_server (fixed) [67]  3  1  45  no  yes  yes  yes  0.03 s  yes 
Double buffering [45]  3  2  16  yes  yes  yes  yes  0.01 s  no 
4.3 Synchronisable Communicating Session Automata
In this section, we study the relationship between synchronisability [9] and kexhaustivity via existential boundedness. Informally, communicating automata are synchronisable if each of their executions can be scheduled in such a way that it consists of sequences of “exchange phases”, where each phase consists of a bounded number of send actions, followed by a sequence of receive actions. The original definition of ksynchronisable systems [9, Definition 1] is based on communicating automata with mailbox semantics, i.e., each automaton has one input queue. Here, we adapt the definition so that it matches our pointtopoint semantics. We write \(\mathcal {A}_!\) for \(\mathcal {A}\cap (\mathcal {C}\times \{!\} \times \varSigma )\), and \(\mathcal {A}_?\) for \(\mathcal {A}\cap (\mathcal {C}\times \{?\} \times \varSigma )\).
Definition 17
(Synchronisability). A valid execution \(\phi = \phi _1 \cdots \phi _n\) is a kexchange if and only if: (1) Open image in new window ; and
(2) \(\forall {\mathtt{pq}} \in \mathcal {C}:\forall 1 \le i \le n :\pi _{{\mathtt{pq}}}^{!}(\phi _i) \ne \pi _{{\mathtt{pq}}}^{?}(\phi _i) \implies \forall i < j \le n :\pi _{{\mathtt{pq}}}^{?}(\phi _j) =\epsilon \).
We write \(\mathcal {A}^* \!\! \parallel _{k}\) for the set of executions that are kexchanges and say that an execution \(\phi \) is ksynchronisable if Open image in new window . A system S is ksynchronisable if each execution in \(\{\phi \, \mid \,\exists s :s_0 \smash {\xrightarrow {\phi }} s \}\) is ksynchronisable.
Condition (1) says that execution \(\phi \) should be a sequence of an arbitrary number of sendreceive phases, where each phase consists of at most 2k actions. Condition (2) says that if a message is not received in the phase in which it is sent, then it cannot be received in \(\phi \). Observe that the bound k is on the number of actions (over possibly different channels) in a phase rather than the number of pending messages in a given channel.
Example 9
Execution \(\phi _1\) is 1bounded for \(s_0\), but it is not a kexchange since, e.g., \( a \) is received outside of the phase where it is sent. In \(\phi _2\), message \( d \) is received outside of its sending phase. In the terminology of [9], this system is not ksynchronisable because there is a “receivesend dependency” between the exchange of message \( c \) and \( b \), i.e., \({\mathtt{p}}\) must receive \( c \) before it sends \( b \). Hence, there is no kexchange that is Open image in new window equivalent to \(\phi _1\) and \(\phi _2\).
Theorem 7
(1) If S is ksynchronisable, then it is \(\exists \)kbounded. (2) If S is ksynchronisable and has the eventual reception property, then it is kexhaustive.
Figure 5 and Table 1 summarise the results of Sect. 4 wrt. \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\) csa. We note that any finitestate system is kexhaustive (and \(\exists \)(S)kbounded) for sufficiently large k, while this does not hold for synchronisability, see Example 9.
5 Experimental Evaluation
We have implemented our theory in a tool [33] which takes two inputs: (i) a system of communicating automata and (ii) a bound \(\textsc {max}\). The tool iteratively checks whether the system validates the premises of Theorem 1, until it succeeds or reaches \(k=\textsc {max}\). We note that the \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\) conditions are required for our soundness result (Theorem 1), but are orthogonal for checking kmc. Each condition is checked on a reduced bounded transition system, called \( RTS _{k}(S)\). Each verification procedure for these conditions is implemented in Haskell using a simple (depthfirstsearch based) reachability check on the paths of \( RTS _{k}(S)\). We give an (optimal) partial order reduction algorithm to construct \( RTS _{k}(S)\) in [43] and show that it preserves our properties.
We have tested our tool on 20 examples taken from the literature, which are reported in Table 2. The table shows that the tool terminates virtually instantaneously on all examples. The table suggests that many systems are indeed kmc and most can be easily adapted to validate bound independence. The last column refers to the gmc condition, a form of synchronous multiparty compatibility (smc) introduced in [39]. The examples marked with Open image in new window have been slightly modified to make them csa that validate \({k}\text {}\textsc {obi}\) and \(\textsc {ibi}\). For instance, we take only one of the possible interleavings between mixed actions to remove mixed states (taking send action before receive action to preserve safety), see [43].
6 Related Work
Theory of communicating automata Communicating automata were introduced, and shown to be Turing powerful, in the 1980s [10] and have since then been studied extensively, namely through their connection with message sequence charts (MSC) [46]. Several works achieved decidability results by using bag or lossy channels [1, 2, 13, 14] or by restricting the topology of the network [36, 57].
Existentially bounded communicating automata stand out because they preserve the fifo semantics of communicating automata, do not restrict the topology of the network, and include infinite state systems. Given a bound k and an arbitrary system of (deterministic) communicating automata S, it is generally undecidable whether S is existentially kbounded. However, the question becomes decidable (pspacecomplete) when S has the stable property. The stable property is itself generally undecidable (it is called deadlockfreedom in [22, 35]). Hence this class is not directly applicable to the verification of message passing programs since its membership is overall undecidable. We have shown that \({k}\text {}\textsc {obi}\), \(\textsc {ibi}\), and kexhaustive csa systems are (strictly) included in the class of existentially bounded systems. Hence, our work gives a sound practical procedure to check whether csa are existentially kbounded. To the best of our knowledge, the only tools dedicated to the verification of (unbounded) communicating automata are McScM [26] and Chorgram [40]. Bouajjani et al. [9] study a variation of communicating automata with mailboxes (one input queue per automaton). They introduce the class of synchronisable systems and a procedure to check whether a system is ksynchronisable; it relies on executions consisting of kbounded exchange phases. Given a system and a bound k, it is decidable (pspacecomplete) whether its executions are equivalent to ksynchronous executions. Section 4.3 states that any ksynchronisable system which satisfies eventual reception is also kexhaustive, see Theorem 7. In contrast to existential boundedness, synchronisability does not include all finitestate systems. Our characterisation result, based on local boundagnosticity (Theorem 3), is unique to kexhaustivity. It does not apply to existential boundedness nor synchronisability, see, e.g., Example 7. The term “synchronizability” is used by Basu et al. [3, 4] to refer to another verification procedure for communicating automata with mailboxes. Finkel and Lozes [19] have shown that this notion of synchronizability is undecidable. We note that a system that is safe with a pointtopoint semantics, may not be safe with a mailbox semantics (due to independent send actions), and viceversa. For instance, the system in Fig. 2 is safe when executed with mailbox semantics.
Multiparty Compatibility and Programming Languages. The first definition of multiparty compatibility appeared in [18, Definition 4.2], inspired by the work in [23], to characterise the relationship between global types and communicating automata. This definition was later adapted to the setting of communicating timed automata in [6]. Lange et al. [39] introduced a generalised version of multiparty compatibility (gmc) to support communicating automata that feature mixed or nondirected states. Because our results apply to automata without mixed states, kmc is not a strict extension of gmc, and gmc is not a strict extension of kmc either, as it requires the existence of synchronous executions. In future work, we plan to develop an algorithm to synthesise representative choreographies from kmc systems, using the algorithm in [39].
The notion of multiparty compatibility is at the core of recent works that apply session types techniques to programming languages. Multiparty compatibility is used in [51] to detect deadlocks in Go programs, and in [30] to study the wellformedness of Scribble protocols [64] through the compatibility of their projections. These protocols are used to generate various endpoint APIs that implement a Scribble specification [30, 31, 48], and to produce runtime monitoring tools [47, 49, 50]. Taylor et al. [67] use multiparty compatibility and choreography synthesis [39] to automate the analysis of the gen_server library of Erlang/OTP. We can transparently widen the set of safe programs captured by these tools by using kmc instead of synchronous multiparty compatibility (smc). The kmc condition corresponds to a much wider instance of the abstract safety invariant \({\varphi }\) for session types defined in [63]. Indeed kmc includes smc (see [43]) and all finitestate systems (for k sufficiently large).
7 Conclusions
We have studied csa via a new condition called kexhaustivity. The kexhaustivity condition is (i) the basis for a wider notion of multiparty compatibility, kmc, which captures asynchronous interactions and (ii) the first practical, empirically validated, sufficient condition for existential kboundedness. We have shown that kexhaustive systems are fully characterised by local boundagnosticity (each automaton behaves equivalently for any bound greater than or equal to k). This is a key requirement for asynchronous message passing programming languages where the possibility of having infinitely many orphan messages is undesirable, in particular for Go and Rust which provide bounded communication channels.
For future work, we plan to extend our theory beyond csa. We believe that it is possible to support mixed states and states which do not satisfy \(\textsc {ibi}\), as long as their outgoing transitions are independent (i.e., if they commute). Additionally, to make kmc checking more efficient, we will elaborate heuristics to find optimal bounds and offload the verification of kmc to an offtheshelf model checker.
Footnotes
 1.
All the benchmarks in this paper were run on an 8core Intel i77700 machine with 16 GB RAM running a 64bit Linux.
Notes
Acknowledgements
We thank Laura Bocchi and Alceste Scalas for their comments, and David Castro and Nicolas Dilley for testing the artifact. This work is partially supported by EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, and EP/N028201/1.
References
 1.Abdulla, P.A., Bouajjani, A., Jonsson, B.: Onthefly analysis of systems with unbounded, lossy FIFO channels. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 305–318. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028754CrossRefGoogle Scholar
 2.Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS 1993, pp. 160–170 (1993)Google Scholar
 3.Basu, S., Bultan, T.: Automated choreography repair. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 13–30. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662496657_2CrossRefGoogle Scholar
 4.Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL 2012, pp. 191–202 (2012)Google Scholar
 5.Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33–58 (2017)MathSciNetCrossRefGoogle Scholar
 6.Bocchi, L., Lange, J., Yoshida, N.: Meeting deadlines together. In: CONCUR 2015, pp. 283–296 (2015)Google Scholar
 7.Bocchi, L., Yang, W., Yoshida, N.: Timed multiparty session types. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 419–434. Springer, Heidelberg (2014). https://doi.org/10.1007/9783662445846_29CrossRefGoogle Scholar
 8.Bollig, B., Kuske, D., Meinecke, I.: Propositional dynamic logic for messagepassing systems. Log. Methods Comput. Sci. 6(3) (2010). https://lmcs.episciences.org/1057
 9.Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 372–391. Springer, Cham (2018). https://doi.org/10.1007/9783319961422_23CrossRefGoogle Scholar
 10.Brand, D., Zafiropulo, P.: On communicating finitestate machines. J. ACM 30(2), 323–342 (1983)MathSciNetCrossRefGoogle Scholar
 11.Castro, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using roleparametric session types in Go: staticallytyped endpoint APIs for dynamicallyinstantiated communication structures. PACMPL 3(POPL), 29:1–29:30 (2019)CrossRefGoogle Scholar
 12.Cécé, G., Finkel, A.: Verification of programs with halfduplex communication. Inf. Comput. 202(2), 166–190 (2005)MathSciNetCrossRefGoogle Scholar
 13.Cécé, G., Finkel, A., Iyer, S.P.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124(1), 20–31 (1996)MathSciNetCrossRefGoogle Scholar
 14.Clemente, L., Herbreteau, F., Sutre, G.: Decidable topologies for communicating automata with FIFO and bag channels. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 281–296. Springer, Heidelberg (2014). https://doi.org/10.1007/9783662445846_20CrossRefGoogle Scholar
 15.Coppo, M., DezaniCiancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146–178. Springer, Cham (2015). https://doi.org/10.1007/9783319189413_4CrossRefGoogle Scholar
 16.Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Form. Methods Syst. Des. 46(3), 197–225 (2015)CrossRefGoogle Scholar
 17.Deniélou, P.M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642288692_10CrossRefGoogle Scholar
 18.Deniélou, P.M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 174–186. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642392122_18CrossRefzbMATHGoogle Scholar
 19.Finkel, A., Lozes, É.: Synchronizability of communicating finite state machines is not decidable. In: ICALP 2017, pp. 122:1–122:14 (2017)Google Scholar
 20.Finkel, A., McKenzie, P.: Verifying identical communicating processes is undecidable. Theor. Comput. Sci. 174(1–2), 217–230 (1997)MathSciNetCrossRefGoogle Scholar
 21.Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput. 204(6), 920–956 (2006)MathSciNetCrossRefGoogle Scholar
 22.Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1–3), 147–167 (2007)MathSciNetzbMATHGoogle Scholar
 23.Gouda, M.G., Manning, E.G., Yu, Y.: On the progress of communications between two finite state machines. Inf. Control 63(3), 200–216 (1984)MathSciNetCrossRefGoogle Scholar
 24.Güdemann, M., Salaün, G., Ouederni, M.: Counterexample guided synthesis of monitors for realizability enforcement. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 238–253. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642333866_20CrossRefzbMATHGoogle Scholar
 25.Hallé, S., Bultan, T.: Realizability analysis for messagebased interactions using sharedstate projections. In: SIGSOFT 2010, pp. 27–36 (2010)Google Scholar
 26.Heußner, A., Le Gall, T., Sutre, G.: McScM: a general framework for the verification of communicating machines. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 478–484. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642287565_34CrossRefzbMATHGoogle Scholar
 27.Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communicationbased programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053567CrossRefGoogle Scholar
 28.Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273–284 (2008)Google Scholar
 29.Hu, R.: Distributed programming using Java APIs generated from session types. In: Behavioural Types: Trom Theory to Tools. River Publishers, June 2017Google Scholar
 30.Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662496657_24CrossRefGoogle Scholar
 31.Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: FASE 2017, pp. 116–133 (2017)CrossRefGoogle Scholar
 32.Jespersen, T.B.L., Munksgaard, P., Larsen, K.F.: Session types for Rust. In: WGP@ICFP 2015, pp. 13–22 (2015)Google Scholar
 33.KMC tool (2019). https://bitbucket.org/julienlange/kmccav19
 34.Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with Mungo and StMungo. In: PPDP 2016, pp. 146–159 (2016)Google Scholar
 35.Kuske, D., Muscholl, A.: Communicating automata (2014). http://eiche.theoinf.tuilmenau.de/kuske/Submitted/cfmfinal.pdf
 36.La Torre, S., Madhusudan, P., Parlato, G.: Contextbounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299–314. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540788003_21CrossRefzbMATHGoogle Scholar
 37.Lange, J., Ng, N., Toninho, B., Yoshida, N.: Fencing off Go: liveness and safety for channelbased programming. In: POPL 2017, pp. 748–761 (2017)Google Scholar
 38.Lange, J., Ng, N., Toninho, B., Yoshida, N.: A static verification framework for message passing in Go using behavioural types. In: ICSE 2018. ACM (2018)Google Scholar
 39.Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: POPL 2015, pp. 221–232 (2015)CrossRefGoogle Scholar
 40.Lange, J., Tuosto, E., Yoshida, N.: A tool for choreographybased analysis of messagepassing software. In: Behavioural Types: from Theory to Tools. River Publishers, June 2017Google Scholar
 41.Lange, J., Yoshida, N.: Characteristic formulae for session types. In: Chechik, M., Raskin, J.F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 833–850. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662496749_52CrossRefGoogle Scholar
 42.Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 441–457. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662544587_26CrossRefzbMATHGoogle Scholar
 43.Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. CoRR, abs/1901.09606 (2019). https://arxiv.org/abs/1901.09606
 44.Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: Haskell 2016, pp. 133–145 (2016)Google Scholar
 45.Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642005909_23CrossRefGoogle Scholar
 46.Muscholl, A.: Analysis of communicating automata. In: Dediu, A.H., Fernau, H., MartínVide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 50–57. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642130892_4CrossRefzbMATHGoogle Scholar
 47.Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. In: FAOC, pp. 1–34 (2017)Google Scholar
 48.Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compiletime API generation for distributed protocols with interaction refinements in F\(\sharp \). In: CC 2018. ACM (2018)Google Scholar
 49.Neykova, R., Yoshida, N.: Let it recover: multiparty protocolinduced recovery. In: CC 2017, pp. 98–108. ACM (2017)Google Scholar
 50.Neykova, R., Yoshida, N.: Multiparty session actors. In: LMCS, pp. 13:1–30 (2017)Google Scholar
 51.Ng, N., Yoshida, N.: Static deadlock detection for concurrent Go by global session graph synthesis. In: CC 2016, pp. 174–184 (2016)Google Scholar
 52.Ng, N., Yoshida, N., Honda, K.: Multiparty session C: safe parallel programming with message optimisation. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 202–218. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642305610_15CrossRefGoogle Scholar
 53.Ocean Observatories Initiative. www.oceanobservatories.org
 54.OMG: Business Process Model and Notation (2018). https://www.omg.org/spec/BPMN/2.0/
 55.Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. In: POPL 2016, pp. 568–581 (2016)CrossRefGoogle Scholar
 56.Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)MathSciNetCrossRefGoogle Scholar
 57.Peng, W., Purushothaman, S.: Analysis of a class of communicating finite state machines. Acta Inf. 29(6/7), 499–522 (1992)MathSciNetCrossRefGoogle Scholar
 58.Perera, R., Lange, J., Gay, S.J.: Multiparty compatibility for concurrent objects. In: PLACES 2016, pp. 73–82 (2016)CrossRefGoogle Scholar
 59.Introduction to protocol engineering (2006). http://cs.uccs.edu/~cs522/pe/pe.htm
 60.Salaün, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. IJBPIM 1(2), 116–128 (2006)CrossRefGoogle Scholar
 61.Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP 2017, pp. 24:1–24:31 (2017)Google Scholar
 62.Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: ECOOP 2016, pp. 21:1–21:28 (2016)Google Scholar
 63.Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. PACMPL 3(POPL), 30:1–30:29 (2019)Google Scholar
 64.Scribble Project homepage (2018). www.scribble.org
 65.Sivaramakrishnan, K.C., Qudeisat, M., Ziarek, L., Nagaraj, K., Eugster, P.: Efficient sessions. Sci. Comput. Program. 78(2), 147–167 (2013)CrossRefGoogle Scholar
 66.Takeuchi, K., Honda, K., Kubo, M.: An interactionbased language and its typing system. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994). https://doi.org/10.1007/3540581847_118CrossRefGoogle Scholar
 67.Taylor, R., Tuosto, E., Walkinshaw, N., Derrick, J.: Choreographybased analysis of distributed message passing programs. In: PDP 2016, pp. 512–519 (2016)Google Scholar
 68.Yellin, D.M., Strom, R.E.: Protocol specifications and component adaptors. ACM Trans. Program. Lang. Syst. 19(2), 292–333 (1997)CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.