Distributed Games with a Central Decision Maker

The design and analysis of concurrent programs and distributed protocols have always presented significant challenges. With the increasing pervasiveness of distributed applications, it is natural to investigate the automated synthesis of such protocols from their specifications. The foundational work on distributed synthesis [19] demonstrated the general undecidability of the problem when processes have access to only purely local information and limited communication capabilities. However, recent works [9, 14, 10, 18, 8, 11, 1] have introduced richer models where processes have access to their entire causal past, broadening the scope of problems that can be tackled. In particular, [9] introduced the notion of causal past and addressed the distributed controller synthesis problem in series-parallel systems and established that controlled reachability is decidable. The work [14] introduced systems with connectedly communicating processes and proved that the MSO theory in this setting is decidable which implies that the associated distributed synthesis problems are decidable.

Two more recent and relevant lines of work are Petri games and asynchronous games. Petri games [8] are distributed games played on Petri nets, where tokens represent players. The places in the underlying Petri net are divided into system and environment places, and tokens in system places make decisions based on their causal history. Several interesting classes of Petri games have been shown to be decidable [8, 7] but it was recently shown in [6] that Petri games with global winning conditions are undecidable, even with only two system players and one environment player.

Asynchronous games [10] are played on deterministic asynchronous automata and allow processes to control actions based on their causal past. These games are shown to be decidable in the interesting setting of acyclic architectures [10, 18] whose underlying process-communication graph is acyclic. More general formulations like decomposable games [11] have also been identified and proven to be decidable. However, the undecidability results for asynchronous games with simple objectives such as local reachability/termination/deadlock-freeness, even in systems with six processes, from [12] highlights the complexity of distributed synthesis problems.

Clearly it is desirable to identify different settings of the distributed synthesis problems which are interesting, practically well motivated and decidable. In this work, we consider the distributed setting in which there is a designated process called the central decision maker. We refer to such distributed systems as CDM systems in which all the key decisions are taken in the presence of this process. In many server-client architectures the server process is primarily responsible for maintaining overall integrity and ensuring that the demands of the client processes are met. These systems serve as prototypical examples of CDM systems. A distributed version control system such as SVN may also be viewed as a CDM system in which a single authoritative main copy is maintained at the central repository. Users make concurrent changes to local copies; in order to effect these changes to the main copy, they acquire an exclusive access to the central repository using a “lock”. One can model this locking mechanism by a central decision maker process which synchronizes with different user processes. Another illustrative example of a CDM system is the working of an institution/organization consisting of multiple agents with a designated head. Various committees are formed to address different aspects of the organization, expedite work and increase overall efficiency. An agent is typically a member of several such committees. These committees conduct procedural meetings from time to time to discuss, gather relevant information and propose solutions. However, all the key decisions are taken in only those committee meetings in which the head participates. The head’s presence in all decision making activities ensures consistency and alignment with the organizational goals. Note that concurrent meetings of different committees are allowed in this example.

In this paper, we formulate and study a distributed CDM game which is played on a non-deterministic asynchronous automaton $A$ involving a team $𝒫$ of processes and assume the presence of a central decision maker, a special process in $𝒫$ which participates in every action which is not deterministic. In these games, the environment manifests itself as a scheduler of actions. Each scheduling decision gives rise to an event which is distributed across the participating processes. These scheduling events inherit a natural partial order in which, for every process, the events in which this process participates, are totally ordered. The processes participating in a scheduled event must respond to the corresponding scheduling choice, purely based on their collective causal past, by providing a matching local transition of $A$. It is important to keep in mind that the environment is simply an abstract scheduler of (possibly concurrent) actions/events and it does not reveal any information about concurrent scheduling choices. In particular, the causal past of the central decision maker contains information only about some scheduling events and gets updated with possibly unbounded information about concurrent scheduling events as the play proceeds. Further, the causal past of any other process may not contain complete information about the decisions taken by the central decision maker. It has access to only those decisions which it learns directly or indirectly through other processes and is oblivious to concurrent scheduling decisions made by the central decision maker.

We show that the key problem of solving a CDM game, that is, deciding the existence of a distributed winning strategy, is efficiently solvable for global safety and local parity winning objectives. We also provide hardness results for these problems which demonstrate that our algorithmic solutions are optimal. More precisely, we show that the problems of solving CDM games for the above objectives are EXPTIME-complete. Our EXPTIME-completeness result for global safety CDM games has some resemblance with a similar result for the Petri game model with one system token studied in [7]. It is important to note that [7] is only concerned with safety objectives. In contrast, we provide a uniform method to address both safety as well as parity objectives. Towards this, we build upon the theory of Mazurkiewicz traces and the theory of two-player games. More precisely, given a CDM game, we associate with it a natural two-player full-information game. Our key result allows to “extract” from a winning strategy in this two-player game, a distributed winning strategy in the CDM game. This is achieved by crucially relying on novel special linearizations of traces that we develop in this work. We believe that these special linearizations have much wider applicability.

This work also formulates a natural notion of a finite-state distributed memory strategy. Such a strategy is modelled as a deterministic asynchronous automaton in which each process keeps track of some additional key information in its local memory states and the responses to scheduling choices are computed with the help of the joint-memory states. The amount of additional local memory provides a measure of the distributed memory complexity of such a finite-state strategy. Recall that, in the standard full-information two-player graph games central to reactive synthesis (see [13]), safety and parity objectives can be achieved by positional/zero-memory winning strategies. In contrast, non-trivial distributed memory is required, in general, for winning global safety and local parity objectives in the CDM setting. For the safety and local parity objectives on CDM games, we establish that existence of distributed winning strategies implies existence of finite-state distributed winning strategies. In fact, we provide a novel construction of a finite-state winning strategy in which each process keeps in its local memory the latest global-state that is part of its causal past. We use the gossip automaton from [17] to maintain and update this information. It turns out that the distributed memory complexity of our construction is exponential in $|𝒫|$ - the number of processes. We also show that this exponential dependence on $|𝒫|$ is unavoidable.

Let us mention that our analysis applies to the more general setting of distributed games in which the “decision” events are causally ordered. In this general setting, any pair of actions, which are not deterministic, must have some process participating in both of them. We thus rule out concurrent/independent actions which are not deterministic. Clearly, this setting includes CDM games as the central decision maker participates in all actions which are not deterministic. Throughout the paper, we mainly address the CDM setting for convenience. Our final result concerns an extension of the CDM model which permits two decision making processes. In this natural extension, in every action which is not deterministic, at least one of the two decision makers participates. We build on the technical machinery of [12] to show the surprizing result that safety games with two decision makers are undecidable.

In this section, we set up basic notations about (Mazurkiewicz) traces (see [4, 3, 16]). A trace is a well-established model of a concurrent behaviour in which the causality and concurrency information between events is represented in the form of a labelled partial order.

Let $𝒫$ be a finite non-empty set of processes, and let $i,j$ range over $𝒫$. We write $\{X_i\}$ for a $𝒫$-indexed family ${\{X_i\}}_{i\in 𝒫}$. A distributed alphabet over $𝒫$ is a family $\tilde{\mathrm{\Sigma }}=\{{\mathrm{\Sigma }}_i\}$ of finite sets. Let $\mathrm{\Sigma }={\bigcup }_{i\in 𝒫}{\mathrm{\Sigma }}_i$ be the total alphabet, i.e., the set of all actions. For $a\in \mathrm{\Sigma }$, we set $\mathrm{loc}(a)=\{i\in 𝒫\mid a\in {\mathrm{\Sigma }}_i\}$ to be the set of processes which participate in it. We let $I=\{(a,b)\in \mathrm{\Sigma }\times \mathrm{\Sigma }|\mathrm{loc}(a)\cap \mathrm{loc}(b)=\mathrm{\varnothing }\}$ and $D=(\mathrm{\Sigma }\times \mathrm{\Sigma })\backslash I$ be the induced independence and dependence binary relations on $\mathrm{\Sigma }$ respectively. For a poset $(X,\le )$ and $Y\subseteq X$, we define $\downarrow Y=\{x\in X\mid x\le y\text{ for some }y\in Y\}$; for $x\in X$, we set $\downarrow x=\downarrow \{x\}$ and $\Downarrow x=\downarrow x\setminus \{x\}$.

Let $t=(E,\le ,\lambda )$ be a trace over $\tilde{\mathrm{\Sigma }}$. The elements of $E$ are referred to as events in $t$. For $e\in E$, $\mathrm{loc}(e)$ abbreviates $\mathrm{loc}(\lambda (e))$. For $i\in 𝒫$, the set of $i$-events in $t$ is $E_i=\{e\in E\mid i\in \mathrm{loc}(e)\}$, i.e., the events in which process $i$ participates. Note that the first condition in the definition of a trace implies that $E_i$ is totally ordered by $\le$. We write $\mathrm{loc}(t)=\{i\in 𝒫\mid E_i\ne \mathrm{\varnothing }\}$ to denote the set of processes which participate in some event in $t$. Note that $\mathrm{loc}(t)={\cup }_{e\in E}\mathrm{loc}(e)$.

Let $\mathrm{TR}(\tilde{\mathrm{\Sigma }})$ denote the set of all traces over $\tilde{\mathrm{\Sigma }}$. As the distribution of $\mathrm{\Sigma }$ across processes will be clear from the context, we use $\mathrm{TR}(\mathrm{\Sigma })$ (or simply $\mathrm{TR}$) instead of $\mathrm{TR}(\tilde{\mathrm{\Sigma }})$. Henceforth a trace means a trace over $\tilde{\mathrm{\Sigma }}$. A trace is finite if the underlying set of events is finite. We use ${\mathrm{TR}}^{\ast }(\mathrm{\Sigma })$ and ${\mathrm{TR}}^{\omega }(\mathrm{\Sigma })$ (or simply ${\mathrm{TR}}^{\ast }$ and ${\mathrm{TR}}^{\omega }$) to denote the set of all finite and infinite traces. Now we describe the concatenation operation on traces. Let $t=(E,\le ,\lambda )$ and $t^{\prime }=(E^{\prime },{\le }^{\prime },{\lambda }^{\prime })$ be finite traces with disjoint event sets $E$ and $E^{\prime }$. We define $t{t}^{\prime }\in {\mathrm{TR}}^{\ast }$ to be the trace $(E^{\prime \prime },{\le }^{\prime \prime },{\lambda }^{\prime \prime })$ where

• $\mathrm{■}$

  $E^{\prime \prime }=E\cup E^{\prime }$,

• $\mathrm{■}$

  ${\le }^{\prime \prime }$ is the transitive closure of $\le \cup {\le }^{\prime }\cup \{(e,e^{\prime })\in E\times E^{\prime }\mid (\lambda (e),{\lambda }^{\prime }(e^{\prime }))\in D\}$,

• $\mathrm{■}$

  ${\lambda }^{\prime \prime }:E^{\prime \prime }\to \mathrm{\Sigma }$ where ${\lambda }^{\prime \prime }(e)=\lambda (e)$ if $e\in E$; otherwise, ${\lambda }^{\prime \prime }(e)={\lambda }^{\prime }(e)$.

Observe that, with $a$ (resp. $b$) denoting the singleton trace whose only event is labelled $a$ (resp. $b$), if $(a,b)\in I$ then $ab=ba$ in ${\mathrm{TR}}^{\ast }$. The trace concatenation operation on finite traces can also be defined for infinite traces under certain conditions. We explain this now. The above mentioned definition of $t{t}^{\prime }$ results in a valid trace if $t$ is finite. That is, if $t\in {\mathrm{TR}}^{\ast }$ and $t^{\prime }\in \mathrm{TR}$ then $t{t}^{\prime }\in \mathrm{TR}$. Moreover, if $t,t^{\prime }\in \mathrm{TR}$ are such that $\omega \mathrm{loc}(t)\cap \mathrm{loc}(t^{\prime })=\mathrm{\varnothing }$, then $t{t}^{\prime }\in \mathrm{TR}$ where $\omega \mathrm{loc}(t)$ is the set of of processes which participate in infinitely many events in $t$. It is easy to see that, in this case, $\omega \mathrm{loc}(t{t}^{\prime })=\omega \mathrm{loc}(t)\cup \omega \mathrm{loc}(t^{\prime })$. We say that a trace $t^{\prime }$ is a prefix of a trace $t$ if $t=t^{\prime }{t}^{\prime \prime }$ for some trace $t^{\prime \prime }$. It is important to observe that this definition permits a prefix to be infinite.

We now come to the very important notion of a configuration of a trace $t=(E,\le ,\lambda )$. A subset $c\subseteq E$ is a configuration of $t$ if $c$ is finite and $\downarrow c=c$. For $e\in E$, $\downarrow e=\downarrow \{e\}$ is the causal past of $e$ and $\Downarrow e=\downarrow e\setminus \{e\}$ is the strict causal past of $e$. Note that, if we restrict the trace $t$ to a configuration $c$, we get another finite trace $t_c=(c,\le ,\lambda )$ which turns out to be a prefix of $t$. Conversely, given a finite prefix $t^{\prime }$ of $t$, we can identify a configuration $c$ of $t$ such that $t^{\prime }=t_c$. In this sense, configurations of $t$ are essentially finite prefixes of $t$. Examples of configurations (or, equivalently, finite prefixes) are the empty set, $\downarrow e$ or $\Downarrow e$, for every event $e\in E$. Note that $E$ itself is a configuration of $t$ iff $t$ is finite. We let $C_t$ denote the set of all configurations of $t$. The action based successor relation ${\to }_t\subseteq C_t\times \mathrm{\Sigma }\times C_t$ is defined by $c{\stackrel{𝑎}{\to }}_t{c}^{\prime }$ if and only if there exists $e\in E$ such that $e\notin c$, $c\cup \{e\}=c^{\prime }$ and $\lambda (e)=a$.

Asynchronous automata and the related transition systems are fundamental finite-state distributed devices due to Zielonka [20, 16] which operate/run on traces. In an asynchronous transition system, each process $i\in 𝒫$ is equipped with a finite non-empty set $S_i$ of local $i$-states. We set $S={\bigcup }_{i\in 𝒫}{S}_i$ and call $S$ the set of local states. Further, we set $S_{𝒫}={\prod }_{i\in 𝒫}{S}_i$ and call it the set of global states. For a non-empty set $P\subseteq 𝒫$ of processes, $S_P={\prod }_{i\in P}{S}_i$ is the set of (joint) $P$-states. For a $P$-state $s\in S_P$ and $i\in P$, $s(i)\in S_i$ denotes the local $i$-state in the $P$-tuple $s$. More generally, for $Q\subseteq P$ and $s\in S_P$, we denote by $s_Q$ the projection of $s$ on $Q$ – that is, $s_Q$ is the unique $Q$-state such that $s_Q(i)=s(i)$ for all $i\in Q$. For $a\in \mathrm{\Sigma }$, we use $a$ to abbreviate $\mathrm{loc}(a)$ when talking about states. Thus $S_a=S_{\mathrm{loc}(a)}$ denotes the set of all $a$-states and if $\mathrm{loc}(a)\subseteq P$ and $s$ is a $P$-state, we write $s_a$ for $s_{\mathrm{loc}(a)}$.

Similar to the convention of writing a $𝒫$-indexed family as $\{X_i\}$, we use the shorthand $\{Y_a\}$ to denote the $\mathrm{\Sigma }$-indexed family ${\{Y_a\}}_{a\in \mathrm{\Sigma }}$.

Let $A=(\{S_i\},\{\stackrel{𝑎}{\to }\})$ be an ATS. Note that a transition in $A$ on an action $a$ is local in the sense that it involves only processes in $\mathrm{loc}(a)$ and $a$-states. We extend these local transition relations naturally to global states. More precisely, for $a\in \mathrm{\Sigma }$, we define $\stackrel{𝑎}{\Rightarrow }\subseteq S_{𝒫}\times S_{𝒫}$ as follows: for $s,s^{\prime }\in S_{𝒫}$, $(s,s^{\prime })\in \stackrel{𝑎}{\Rightarrow }$ if $(s_a,s_a^{\prime })\in \stackrel{𝑎}{\to }$ and $s_{𝒫\setminus \mathrm{loc}(a)}=s_{𝒫\setminus \mathrm{loc}(a)}^{\prime }$. An action $a$ is said to be enabled at $s\in S_{𝒫}$ if there exists $s^{\prime }\in S_{𝒫}$ such that $(s,s^{\prime })\in \stackrel{𝑎}{\Rightarrow }$. Due to the locality of transitions, if $a$ is enabled at $s$, then it is also enabled at $s^{\prime }$ with $s_a=s_a^{\prime }$.

Now we define the important notion of a run of $A$ on a trace $t$ over $\tilde{\mathrm{\Sigma }}$. Let us fix an initial global state $s_0\in S_{𝒫}$. A run of $A$ on $t\in \mathrm{TR}$, starting from $s_0$, is a map $\rho :C_t\to S_{𝒫}$ such that $\rho (\mathrm{\varnothing })=s_0$ and for every $c,c^{\prime }\in C_t$, $c{\stackrel{𝑎}{\to }}_t{c}^{\prime }$ implies that $(\rho (c),\rho (c^{\prime }))\in \stackrel{𝑎}{\Rightarrow }$. Note that, as $A$ is non-deterministic, there can be multiple runs of $A$ on the same trace. The following lemma follows directly from the locality of transitions of $A$.

Now we describe the model called asynchronous transition system games or simply ATS games. ATS games on two processes are studied in [1]. An ATS game is played on a non-deterministic asynchronous transition system between an environment and a distributed system that comprises of a team of cooperating processes. The environment is a singular entity and manifests itself in the form of a scheduler of actions. Importantly, the environment does not reveal any information about prior/concurrent scheduling events.

We continue with the notation from the previous section. In particular, we fix a distributed alphabet $\tilde{\mathrm{\Sigma }}$ over a fixed set $𝒫$ of processes.

A play of an ATS game is inherently distributed, capturing the ongoing, possibly non-terminating interaction between the distributed system and the environment. Let us now formalize this notion of a distributed play. To this end, fix an ATS game $𝒢=(A,s_0,\mathrm{Win})$ with $A=(\{S_i\},\{\stackrel{𝑎}{\to }\})$.

We begin with a description of the interleaved semantics of a distributed play. Such a play begins in the initial global state $s_0$. Environment makes the first move by scheduling an action (say $a$) which is enabled at $s_0$. The processes participating in $a$ respond by selecting an available $a$-transition and thus advancing the “current” global state (say, to $s$). At this point, it is environment’s turn to schedule another action (say $b$) which is enabled at $s$. The processes participating in $b$ respond by choosing a suitable $b$-transition at $s$. Let us assume that $a$ and $b$ are independent actions. Then the processes participating in $b$ are oblivious to the “concurrent” scheduling of “prior” $a$-action. It is important to observe that, in this situation, thanks to the locality of transitions in $A$, $b$ is also enabled at $s_0$ and environment also had the option of scheduling $b$ first and then $a$ later. On the other hand, if $a$ and $b$ are dependent, then there is a process which participates in both $a$ and $b$ and every process participating in $b$ comes to know about the prior $a$-action which is “causally” before the current $b$-action.

So, in this interleaved semantics of a distributed play, a play consists of an alternate sequence of moves of the environment (which schedules actions) and the distributed system (where the participating processes respond by matching transitions). Observe that each process in the distributed system has only partial information; among all the actions which are already scheduled, it only knows those which are in its causal past. The causal past of a process contains the information that a process comes to know directly or indirectly through its interactions with the other processes. Further when two or more processes interact (by participating in a shared/joint action), they exchange their complete causal pasts.

The idea is that the (labelled) events in $t$ represent enabled scheduler choices and the partial-order $\le$ captures the causality between these events arising out of the distribution of these events across processes. The fact that an event $e$ is labelled $a$ (that is, $\lambda (e)=a$) means that the environment scheduled the shared action $a$ which lead the processes participating in $a$ to synchronize. Their collective causal past-information at $e$ corresponds to events in $\Downarrow e$. Based on this common information, these processes respond to $e$ by choosing a local transition on $a$ which advances their prior joint $a$-state $s_a$ to $s_a^{\prime }$ where $s=\rho (\Downarrow e)$ and $s^{\prime }=\rho (\downarrow e)$. Thus the run $\rho$ correctly captures the decisions of the processes during the play. Note that by Lemma 5, $\rho$ is completely determined by $\rho (\mathrm{\varnothing })=s_0$ and $\rho (\downarrow e)$ for each $e\in E$. In summary, the event $e$ models environment’s scheduling of action $\lambda (e)$ at the global state $\rho (\Downarrow e)$; and the $\lambda (e)$-transition from $\rho (\Downarrow e)$ to $\rho (\downarrow e)$ models the collective response of the processes participating in $e$.

A (distributed) play $(t,\rho )$ is said to be maximal if there is no play $(t^{\prime },{\rho }^{\prime })$ such that $t$ is a proper prefix of $t^{\prime }$ and $\rho ={{\rho }^{\prime }|}_{C_t}$, the restriction of ${\rho }^{\prime }$ to the configurations of $t$. Note that if $(t,\rho )$ is maximal then the processes which have moved only finitely often in $t$ can not be further scheduled by the environment as no action involving only them is enabled. It is important to note that a maximal play could be either finite or infinite. If a maximal play $(t=(E,\le ,\lambda ),\rho )$ is finite, then no action is enabled at the final global state $\rho (E)$.

We next turn our attention to the winning condition $\mathrm{Win}$ which specifies the winner of a maximal play. At an abstract level, $\mathrm{Win}$ is simply the collection of all maximal plays in which the distributed system wins.

In this work we study ATS games from the viewpoint of decision making processes.

Now we are ready to define the important and crucial notion of a distributed strategy for an ATS game. Intuitively speaking, a distributed strategy is an advice function that the team of processes in the distributed system uses to respond to environment’s actions. More importantly, this response can only depend on the collective causal history of the processes participating in this action. Further, the advice function does not restrict the choices available to the environment in all situations.

It is easy to see that the first condition in the above definition, that the domain of $\sigma$ is prefix-closed, is redundant. By requiring $\sigma$ to have the smallest domain, the second and third conditions in the above definition ensure that $\sigma$ becomes defined exactly on traces built by iteratively extending the empty trace along enabled actions, making the domain of $\sigma$ prefix-closed.

A finite trace $t=(E,\le ,\lambda )\in {\mathrm{TR}}^{\ast }$ is said to be prime if $t$ has a unique maximum event. In other words, a prime trace $t$ has an event $e\in E$ such that $E=\downarrow e$; we let $\mathrm{last}(t)$ denote this maximum event of $t$. The next lemma states that a distributed strategy is determined by its effect on the prime traces.

The description at the end of Example 9, for the CDM game in Figure 2, can be readily converted into a winning distributed strategy as in the above definition.

Given an ATS game $𝒢=(A,s_0,\mathrm{Win})$, the key algorithmic question is to decide if there exists a distributed winning strategy in $𝒢$. We answer this for CDM games with global safety and local parity conditions. Note that a CDM game is a partial-information game and different processes have mutually incomparable partial informations about scheduler’s actions; a process is oblivious to concurrent scheduling decisions on other processes and there is no bound on the number of such concurrent scheduling decisions. Clearly the decisions taken by the central decision maker (based solely on its causal past) influence the future behaviour of other processes. Observe that ATS games with only one process ($|𝒫|=1$) are CDM games and are essentially full-information two-player games played on a finite graph [13].

We now develop a general construction which aids in the solution of CDM games. Let us fix a CDM game $𝒢=(A,s_0,\mathrm{Win})$ with $A=(\{S_i\},\{\stackrel{𝑎}{\to }\})$ and process $1\in 𝒫$ as the central decision maker. Towards solving $𝒢$, we introduce a standard full-information two-player game $G_{\mathrm{seq}}$ played on a finite graph $A_{\mathrm{seq}}$ between two players called $\mathrm{Sys}$ and $\mathrm{Env}$. See [13] for a study of these games and its relevance to reactive synthesis in the sequential setting.

We define $G_{\mathrm{seq}}=(A_{\mathrm{seq}},s_0,{\mathrm{Win}}_{\mathrm{seq}})$ to be a standard two-player graph game of complete information whose winning condition ${\mathrm{Win}}_{\mathrm{seq}}$ is currently unspecified. Note that $s_0\in V_{\mathrm{env}}$. The game $G_{\mathrm{seq}}$ is played by players $\mathrm{Sys}$ and $\mathrm{Env}$ by alternately moving a “token” along the edges of the bipartite graph $A_{\mathrm{seq}}$. Player $\mathrm{Env}$ makes moves from $V_{\mathrm{env}}$ and player $\mathrm{Sys}$ makes moves from $V_{\mathrm{sys}}$. Initially the token is at vertex $s_0\in V_{\mathrm{env}}$. Thus a play of $G_{\mathrm{seq}}$ is a sequence (possibly infinite) of vertices visited by the token starting with vertex $s_0$ and it is of the form: $s_0,(s_0,a_0),s_1,(s_1,a_1),s_2,\mathrm{\dots }$. A maximal play is either infinite, or finite in which case it ends in $s\in V_{\mathrm{env}}$ such that no action is enabled at $s$ and as a result, there is no outgoing-edge in $A_{\mathrm{seq}}$ from the vertex $s$. As mentioned above, we do not specify the winning condition ${\mathrm{Win}}_{\mathrm{seq}}$ in this section and it will be suitably instantiated in later sections.

It will be useful to view a play of $G_{\mathrm{seq}}$ as simply a sequence $s_0,a_0,s_1,a_1,s_2,\mathrm{\dots }$ starting at $s_0$ such that, for each $i$, $a_i$ is enabled at $s_i$ and $(s_i,s_{i+1})\in \stackrel{a_i}{\Rightarrow }$. In this viewpoint, $a_i$ corresponds to player $\mathrm{Env}$ moving the token from $s_i$ to $(s_i,a_i)$ and, $s_{i+1}$ corresponds to player $\mathrm{Sys}$ moving the token subsequently from $(s_i,a_i)$ to $s_{i+1}$.

A (sequential full-information) strategy for player $\mathrm{Sys}$ in $G_{\mathrm{seq}}$ maps its history leading to current vertex to the next valid vertex. We formalize it as follows.

Henceforth, by a strategy in $G_{\mathrm{seq}}$ we always mean a strategy for the player $\mathrm{Sys}$ in $G_{\mathrm{seq}}$. It turns out that every distributed strategy in $𝒢$ naturally gives rise to a sequential strategy in $G_{\mathrm{seq}}$. We develop some more notation to explain this. Each finite word $w\in {\mathrm{\Sigma }}^{\ast }$ naturally induces a finite trace $t\in {\mathrm{TR}}^{\ast }$. More precisely, if $w=a_1{a}_2\mathrm{\cdots }{a}_n$, we associate with $w$ the finite trace $t=(E,\le ,\lambda )$ which is defined as follows: $E=\{e_1,e_2,\mathrm{\dots },e_n\}$ has $n$ events corresponding to $n$ positions in the word $w$; we set $\lambda (e_i)=a_i$ and the partial order $\le$ on $E$ is the transitive-closure of the relation $\{(e_i,e_j)|i\le j\text{ and }(a_i,a_j)\in D\}$. It is easy to check that $t$ is indeed a trace over $\tilde{\mathrm{\Sigma }}$. Let us denote this association by the map $\eta :{\mathrm{\Sigma }}^{\ast }\to {\mathrm{TR}}^{\ast }$. It turns out [4, 3, 16] that for a trace $t\in {\mathrm{TR}}^{\ast }$, the set ${\eta }^{-1}(t)\subseteq {\mathrm{\Sigma }}^{\ast }$ is precisely all those words which correspond to different linearizations of $t$. In fact, $\eta$ is a surjective monoid morphism and $\eta (w)=\eta (w^{\prime })$ iff $w$ can be obtained from $w^{\prime }$ by a sequence of operations where each operation is an exchange of two adjacent independent letters.

The next proposition states that, a distributed strategy $\sigma$ in $𝒢$ naturally induces a (sequential) strategy ${\sigma }_{\mathrm{seq}}$ in $G_{\mathrm{seq}}$.

So, the strategies in $G_{\mathrm{seq}}$ induced by distributed strategies in $𝒢$ are diamond-closed. However, an arbitrary strategy in $G_{\mathrm{seq}}$ is not necessarily diamond-closed.

Our main goal in this section is to extract a distributed strategy in $𝒢$ from an arbitrary strategy crucially exploiting the presence of a central decision maker. Towards this, we now develop special linearizations of finite traces.

We first fix a total order ${⊲}_{\mathrm{\Sigma }}$ on $\mathrm{\Sigma }$ such that $\mathrm{\Sigma }\setminus {\mathrm{\Sigma }}_1{⊲}_{\mathrm{\Sigma }}{\mathrm{\Sigma }}_1$. Note that, in the total order ${⊲}_{\mathrm{\Sigma }}$, if $a,b\in \mathrm{\Sigma }$ are such that $1\notin \mathrm{loc}(a)$ and $1\in \mathrm{loc}(b)$ then $a{⊲}_{\mathrm{\Sigma }}b$. With our implicit assumption that process $1$ is the central decision maker, every action in which it does not participate comes before every action in which it participates in the order ${⊲}_{\mathrm{\Sigma }}$. We now outline an inductive procedure to compute a special linearization map $\mathrm{Lin}:{\mathrm{TR}}^{\ast }\to {\mathrm{\Sigma }}^{\ast }$.

In short, we compute $\mathrm{Lin}(t)$ starting from its last action/letter. Towards this, we peel off that maximal event of $t$ which is ${⊲}_{\mathrm{\Sigma }}$-least labelled and put its label as the last letter in $\mathrm{Lin}(t)$ and continue this process until all events are covered.

Now we exploit the key consequences of the ${⊲}_{\mathrm{\Sigma }}$ requirement that $\mathrm{\Sigma }\setminus {\mathrm{\Sigma }}_1{⊲}_{\mathrm{\Sigma }}{\mathrm{\Sigma }}_1$. It is very important to observe that, in general, $t^{\prime }$ is a trace-prefix of $t$ does not imply that $\mathrm{Lin}(t^{\prime })$ is a word-prefix of $\mathrm{Lin}(t)$. The following lemma plays a crucial role later.

Now we use special linearizations to lift a strategy in $G_{\mathrm{seq}}$ to a distributed strategy in $𝒢$. Intuitively, in the special linearization of a trace, all the events of process $1$ appear the earliest. Thus the response of a sequential strategy along the special linearization is based on the least amount of information to the central decision maker. We lift these responses to construct a distributed strategy.

Let us illustrate the above definition for the non-diamond-closed strategy $\tau$ from Example 17 with $t$ being the trace induced by the word $a{d}_2{d}_{3}c$. As $\mathrm{Lin}(t)=a{d}_{2}c{d}_3$, we set ${\tau }_{\mathrm{dstr}}(t)=\tau (a{d}_{2}c{d}_3)=LBB$. Note that $\tau (a{d}_2{d}_{3}c)=RBB$.

We now state the following main proposition which shows that partial function ${\tau }_{\mathrm{dstr}}$ from Definition 21 is in fact a distributed strategy in $𝒢$. The proof crucially uses Lemma 19 which implies that, restricted to central decision maker events, special linearization of a later event extends that of an earlier one.

We turn our attention to CDM games with global safety and local parity objectives. For an ATS $A=(\{S_i\},\{\stackrel{𝑎}{\to }\})$, ${\max }_i|S_i|$ denotes the maximum number of local states per process. For complexity analysis, we make the realistic assumption that every action involves at most a fixed constant number of participating processes. This is reasonable because in most distributed systems, each action involves only a few processes interacting at a time, e.g., reading/writing shared resources or coordinating with immediate “neighbors”. Thanks to this assumption and the local nature of transitions of $A$, it is easy to check that the size of $A$, denoted by $\Vert A\Vert$, is polynomial in ${\max }_i|S_i|$, $|\mathrm{\Sigma }|$ and $|𝒫|$. Besides $\Vert A\Vert$, the other component which contributes to the size of a CDM game $𝒢$, denoted $\Vert 𝒢\Vert$, is the specification of the winning condition. Observe that the number of vertices in the game arena $A_{\mathrm{seq}}$ (see Definition 13) is atmost $2\ast |\mathrm{\Sigma }|\ast {({\max }_i|S_i|)}^{|𝒫|}$. Note that ${({\max }_i|S_i|)}^{|𝒫|}$ is the maximum number of global-states of $A$. As a result, the size of $A_{\mathrm{seq}}$, denoted by $\Vert A_{\mathrm{seq}}\Vert$ is polynomial in ${({\max }_i|S_i|)}^{|𝒫|}$ and $|\mathrm{\Sigma }|$.

In this section we investigate distributed strategies in CDM games which admit a finite-state implementation. Let $𝒢=(A,s_0,\mathrm{Win})$ be an ATS game with $A=(\{S_i\},\{\stackrel{𝑎}{\to }\})$.