Paper deep dive
Decoupled Planning for Multiple Omega-Regular Objectives
Guy Avni, Thomas A. Henzinger, Kaushik Mallik, Suman Sadhukhan, K. S. Thejaswini
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/8/2026, 2:56:53 PM
Summary
The paper introduces a decoupled planning framework for generating graph paths that satisfy multiple ω-regular objectives. Independent agents select local policies for individual objectives, while a scheduler dynamically composes them into a single path. The study shows that deterministic schedulers fail to guarantee correctness, stochastic schedulers are necessary but insufficient without coordination, and introduces 'conventions' (a priori policy restrictions) to ensure satisfaction for safety, Büchi, co-Büchi, and parity objectives.
Entities (10)
Relation Signals (9)
Decoupled Framework → uses → Scheduler
confidence 97% · We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler -- oblivious to the graph and objective -- dynamically composes these policies into a single path.
Deterministic Scheduler → failstoensure → δ-correctness
confidence 96% · We show that even extremely fair deterministic schedulers do not ensure correctness
Conventions → guarantee → Satisfaction of all objectives
confidence 96% · conventions -- simple, a priori restrictions agreed upon before the graph or objectives are revealed -- that guarantee satisfaction of all objectives when followed by all agents.
Büchi Objectives → admit → Universal composition of finite-memory policies
confidence 95% · Büchi objectives admit universal composition of finite-memory policies without scheduler communication
Scheduler → composes → Agent policies
confidence 95% · a scheduler -- oblivious to the graph and objective -- dynamically composes these policies into a single path.
Stochastic Scheduler → requiredfor → δ-correctness
confidence 94% · stochastic schedulers, while necessary, are insufficient without coordination.
Safety Objectives → require → Protocol for synchronizing on maximal safe actions
confidence 93% · For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We study the problem of generating paths on a graph that satisfy a collection of {\omega}-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler -- oblivious to the graph and objective -- dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions -- simple, a priori restrictions agreed upon before the graph or objectives are revealed -- that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of {\omega}-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.
Tags
Links
- Source: https://arxiv.org/abs/2605.13185v1
- Canonical: https://arxiv.org/abs/2605.13185v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
116,733 characters extracted from source content.
Expand or collapse full text
11institutetext: Department of Computer Science, University of Haifa, Israel 11email: gavni@cs.haifa.ac.il22institutetext: Institute of Science and Technology Austria, Klosterneuberg, Austria 22email: tah@ista.ac.at33institutetext: IMDEA Software Institute, Spain 33email: kaushik.mallik@imdea.org44institutetext: Clausthal University of Technology, Germany 44email: suman.sadhukhan@tu-clausthal.de55institutetext: Université Libre de Bruxelles, Belgium 55email: thejaswini.raghavan@ulb.be Decoupled Planning for Multiple Omega-Regular Objectives†thanks: This work is funded by the following grants: European Research Council under Grant No.: ERC-2020-AdG 101020093, ISF grant no. 1679/21, grant RYC2024-049116, MICIU/AEI/10.13039/501100011033, the ESF+, and Volkswagen Foundation within its Momentum framework under project no. 9C283. The last author was employed at Institute of Science and Technology Austria for part of this work. Guy Avni Thomas A. Henzinger Kaushik Mallik Suman Sadhukhan K. S. Thejaswini Abstract We study the problem of generating paths on a graph that satisfy a collection of ω-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of ω-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled. 1 Introduction The graph traversal problem takes as input a finite directed graph and a temporal specification over sequences of vertices, and the goal is to compute a traversal policy for selecting the next vertex based on the history of the past vertices, such that the resulting infinite path fulfills the given specification. A primary application of graph traversal is robotic path planning [16], and other applications include parsing natural languages using stochastic grammars [20], and informational search with online learning [19]. Often, the specification requires simultaneous fulfillment of multiple, competing objectives; for example, a robot may need to simultaneously patrol a given location and visit the charging station intermittently. The traditional approach to solve such problems is to compute a single, monolithic policy for the conjunction of all objectives. In this paper, we introduce a decoupled framework for graph traversals. Consider a collection of objectives φ1,…,φN _1,…, _N that a path needs to satisfy. We describe the framework as an interaction among N agents. For 1≤i≤N1≤ i≤ N, Agent i is only responsible for satisfying objective φi _i and does so by selecting a policy that achieves φi _i. At runtime, a fixed scheduler composes the policies by scheduling one of the agents to choose the next vertex at each step. Our goal is to ensure that the path generated by the composition satisfies all objectives (either deterministically or almost surely) while achieving maximal decoupling by keeping the agents’ choices and scheduler as independent as possible. Before we make these goals more concrete and discuss the features that they lead to, we first illustrate the framework and its challenges. ℓ 1t_1t2t_2startrrb2b_2b1b_1 Fig. 1(a) Reachability objectives given by T1=ℓT_1= \ \ and T2=rT_2= \r \, and policies π1 _1 dashed red and π2 _2 dotted blue. vvstarta1a_1b1b_1a2a_2b2b_2 Fig. 1(b) A graph with two Büchi objectives given by accepting vertices T1=b1T_1= \b_1 \ and T2=b2T_2= \b_2 \. Example 1 Consider a coffee-serving robot in an office modeled as in Fig. 1(a). The objective φ1 _1 requires “reach and serve coffee at ℓ ” and the objective φ2 _2 requires “reach r.” Suppose Agent 11 and Agent 22 choose policies π1 _1 and π2 _2 that always take the shortest paths towards their respective goal states. Clearly, if the robot follows only π1 _1 or only π2 _2, respectively, φ1 _1 and φ2 _2 are satisfied. We describe two schedulers for composing the policies at runtime. First, consider a deterministic scheduler σ _ d that alternates between π1 _1 and π2 _2: at odd time steps, the robot follows π1 _1, and at even time steps, it follows π2 _2. The composition does not satisfy either objective. For example, the path starting from t2t_2 forever alternates between t1t_1 and t2t_2. Notably, σ _ d fulfills the extreme fairness property [25], because each agent is given control infinitely often. The example shows that in order to guarantee that all objectives are satisfied, our framework requires schedulers with an even stronger form of fairness. Now consider a stochastic scheduler σ _ s that, at each point in time, chooses which policy to follow uniformly at random. This scheduler fulfills a stronger notion of fairness, called probabilistic fairness [12] (also related to α-fairness [26]). The composition of π1 _1 and π2 _2 using σ _ s now generates a random path that almost surely visits each of ℓ,t1,t2 ,t_1,t_2, and r infinitely often, thus both objectives are satisfied almost surely. ∎ We postpone the justification of our design choices of schedulers and policies until the end of the introduction. The advantages of our new framework stem from its modularity; it enables a separation of concerns in designing policies and allows changing, deleting, or adding any number of policies without any extra computational overhead, offering a lightweight, plug-and-play composition operation. We point out specific advantages over the monolithic approach: (i) parallel design: each policy is designed independently, which enables, for example, designed on separate CPUs to increase scalability, or by different vendors increasing flexible design; (i) robustness: when an objective changes, only the relevant module needs to change and the other modules can stay fixed; (i) iterative design: a realistic design procedure often requires addition of objectives to the original objectives, which can be simply added as a new module; (iv) dynamic changes: our framework allows deleting or adding objectives to a system that has already been deployed (a “patch”). The first step of our decoupled synthesis addresses the safety components of the individual objectives. Given a graph G and an objective φ , we can use standard procedure to decompose φ into safety and liveness components, writing φ=φ∩φ = safe∩ live, where φ safe requires some unsafe vertices to be avoided at all time, and φ live requires some good event to eventually occur. We show that φ safe cannot, in general, be guaranteed under stochastic scheduling without additional communication. To this end, we propose a protocol in which agents communicate their sets of safe actions at each step, and the scheduled agent is required to select an action from the intersection of these sets. Under mild assumptions, we prove that this protocol suffices to ensure satisfaction of each safety objective at all times. Once safety is enforced, we remove all unsafe edges from the graph and exclusively focus on the liveness objectives in the resulting subgraph. For clarity of exposition, we assume this graph is strongly connected, although this assumption is not essential and will be relaxed later. We first study the existence of a stochastic scheduler that composes any collection of policies in a way that the composition almost-surely satisfies all liveness objectives. Somewhat surprisingly, we show that, already for Büchi objectives in strongly-connected graphs, such “universal” schedulers does not exist. We sketch the intuition in the following example, and details can be found in Thm. 5. Example 2 Consider the graph depicted in Fig. 1(b). We describe two policies π1 _1 and π2 _2 respectively for the Büchi objectives φ1 _1 and φ2 _2 given by target vertices b1\b_1\ and b2\b_2\. Consider an exponentially increasing sequence, e.g., n0=1n_0=1 and nj=2⋅nj−1n_j=2· n_j-1, for j≥1j≥ 1. Define π1 _1 as follows, and π2 _2 is dual. When not at a1a_1, proceed towards b2b_2, and when at a1a_1 at time t, if t=njt=n_j, for j≥0j≥ 0, proceed to b1b_1, otherwise stay at a1a_1. That is, π1 _1 spends exponentially increasing time at a1a_1; visits to b1b_1 become exponentially rare. Clearly, if πi _i operates alone, it satisfies φi _i, for i∈1,2i∈ \1,2 \. Consider a scheduler that at each point in time, chooses which policy acts uniformly at random. Intuitively, the probability that a random walk visits aia_i, for i∈1,2i∈ \1,2 \, precisely at a time njn_j, for some j≥1j≥ 1, is exponentially decreasing, which implies that the probability of visiting bib_i infinitely often tends to a constant, thus φ1∧φ2 _1 _2 is not satisfied almost surely. In Thm. 5, we generalize the construction to any stochastic scheduler. ∎ Example 2 shows that if the agents are allowed to choose any unrestricted policies, there exist situations when the composition will violate the individual objectives. We submit that if all the agents are made to choose policies according to some suitable convention, the composition will be guaranteed to satisfy all objectives, almost surely. For example, for Büchi objectives, we show that the convention of choosing only finite-memory policies guarantee the fulfillment of all individual objectives. We formalize conventions as mappings from classes of objectives (Büchi, co-Büchi, etc.) to restrictions on policies (finite-memory, etc.). Importantly, the restrictions need to be finalized before seeing the specific graph and objectives at hand, setting our framework apart from the joint design of coordinated policies. This way, the modularity requirement is achieved: agents can independently design their policies based on the respective conventions, and addition, modification, or removal of policies do not affect the rest of the policies. Conventions can be intuitively explained using a simple metaphor, whose inspiration comes from the work of Lewis [23]. Suppose two friends want to meet, but they are unable to talk to each other and arrange the location. Convention dictates that each of them should go to the place where they most often meet, and if both parties follow the same convention, they will successfully meet. In essence, convention is a way of inducing coordination when direct communication is not possible. Coming back to our framework, conventions help agents achieve their objectives without directly synchronizing their policies with each other. Our goal is to establish minimally restrictive conventions for different classes of ω-regular objectives. While the convention for Büchi objectives was merely to use finite-memory policies, the same does not suffice anymore for co-Büchi objectives, as we illustrate using the following example. Example 3 Consider the graph that is depicted in Fig. 1(a) and two co-Büchi objectives: FGℓFG\, , requiring eventually staying in ℓ , and FG(ℓ∨r)FG\,( r), requiring eventually staying in either ℓ or r. Observe that for i∈1,2i∈ \1,2 \, following the finite-memory policy πi _i (depicted also in Fig. 1(a) in dashed red and dotted blue) results in a path that satisfies the respective objective, but a random composition of the two visits both t1t_1 and t2t_2 infinitely often, almost surely, and thus violates both objectives. ∎ The challenge behind co-Büchi convention is that in order to satisfy a conjunction of co-Büchi objectives, all policies—that are oblivious to each other’s target vertices—must eventually converge into a common cycle that is good for everyone. We describe a convention for co-Büchi objectives in strongly-connected graphs. Given a co-Büchi objective φi _i, Agent i chooses a policy πi _i that operates as follows. (1) Randomly choose a lasso-shaped path ρi=ρi⋅Ciωρ^i= _i· C_i^ω, where CiC_i is a cycle that satisfies φi _i. This is Agent i’s guess of the common path everyone is trying to follow. (2) If scheduled at vertex v: choose the successor v′v of v on ρiρ^i. (3) If not scheduled: observe the next vertex u, and if u≠v′u≠ v , a conflict is observed: return to Step (1) and sample a new path. Example 4 Consider again the objectives over the graph depicted in Fig. 1(a) φ1=FGℓ _1=FG\, and φ2=FG(ℓ∨r) _2=FG\,( r), the initial position is t1t_1, and let the choice of lasso paths be ρ1=t1ℓωρ^1=t_1 ^ω and ρ2=t1t2rωρ^2=t_1t_2r^ω. Observe that ρiρ^i satisfies φi _i for each i. Suppose that π1 _1 is scheduled and proceeds to ℓ . Thus, π2 _2 observes a conflict (it expects the next vertex to be t2t_2), and randomly chooses an alternative lasso path that satisfies φ2 _2. Correctness follows from a measure-theoretic argument: If there exists a common path that satisfies all co-Büchi objectives, then there also exists a lasso-shaped path that does the same. Random scheduling implies that eventually and almost surely the policies will stabilize in a lasso-shaped path where no policies will change their guesses anymore. ∎ We develop sufficient conventions for major classes of ω-regular objectives, including safety, Büchi, co-Büchi, and parity, and consider path planning problems on both strongly connected and general graphs. As the objectives become more complex, the conventions become more demanding, as expected. Although our conventions are simple to describe, their correctness proofs involve intricate measure-theoretic arguments. With this, we create the foundation of a first-of-its-kind modular design framework for ω-regular decision-making. Design choices. We discuss the design choices of our framework. (i) Independent policy choice. In all our conventions, an agent chooses a policy without knowing the objectives of the other agents. This enables robustness: when objective φj _j changes, Agent i does not need to change their policy. (i) Minimal runtime coordination. For Büchi objectives, conventions choose traditional policies (later called path-aware policies) that use no runtime coordination (see π1 _1 and π2 _2 in Example 1). This means that agents can apply off-the-shelf tools to design policies, and different agents can even apply different techniques, e.g., reinforcement learning or formal techniques. For co-Büchi objectives, policies know which time steps they are scheduled in. Importantly, such policies are not aware of the number of agents, meaning that additional objectives can be added (offline or at runtime) without changing the policy. (i) Graph-independent schedulers. To motivate this, we return to Example 1. Intuitively, composition using the deterministic scheduler σ _ d failed because none of the agents were getting enough time to reach their target. A naïve fix simply schedules each policy three times in a row. While this does solve the problem at hand, it is an ad hoc solution that will break if either graph or objectives change. Alternatively, one could consider a nondeterministic scheduler and construct policies that fulfill their objectives no matter how the nondeterminism is resolved. Unfortunately, this is too restrictive from the policy design standpoint: in Example 1, given the policies π1 _1 and π2 _2, a nondeterministic scheduler can act like an adversary and find an interleaving of the policies (like the one of σ _ d) such that the path keeps cycling between t1t_1 and t2t_2 and never visits the targets. Defeating such an adversarial scheduler is possible, but would require the policies to take joint actions (like π1 _1 and π2 _2 making a clockwise traversal of the graph in Example 1), which would preclude the key aspect of modular design. (iv) Simple schedulers. We see it as a feature of our framework that our schedulers are simple and can thus run on devices with limited processing capabilities like robots or drones. Related Work Computing policies for multi-objective decision-making problems is a well-studied problem, both for probabilistic [5, 6, 11] and non-probabilistic [27] systems. Almost all works produce a single, monolithic policy that fulfills all objectives. Decoupling has been considered in other fields with the same motivation as us; a framework that is modular, robust, and separates design concerns. For example, decoupling exploration from exploitation has been studied in RL [28], behavioral programming is a decoupled approach to programming [17], decoupling has been applied in control [15], and game theory [18]. We compare with two approaches for decoupled design that are closest to our work. The first kind “over-approximates” the local policies using the so-called strategy templates [2], which abstractly represent sets of policies that would fulfil the objectives.111Strategy templates are originally developed on turn-based game graphs, which are generalizations of the plain graphs that we use in this work. When these local strategy templates are composed, we obtain a strategy template for the conjunction of all objectives, from which a concrete policy for the overall problem can be extracted. Unfortunately, the composition of strategy templates is computationally intensive, which creates substantial computational overhead and can impact the runtime performance of the composed policy. The second kind of modular design uses auctions as a scheduler, and is called auction-based scheduling (ABS) [4]: Each policy starts with a budget, and at each step, an auction is held, where the policies use their available budgets to bid for the privilege of selecting the next action. Bidding policies for ABS are found by independently solving a two-player zero-sum bidding game [22, 3]. We point to two key advantages of our approach over ABS. First, our approach allows an arbitrary number of objectives whereas ABS for multiple objectives is currently not possible due to the dependency on multi-player bidding games, which, to best of our knowledge, have not yet been studied. Second, ABS is a sound but incomplete method: it is possible that there is a path that satisfies both objectives, but there is no decoupled solution for ABS. In fact, most instances with a pair of co-Büchi objectives cannot be decoupled using ABS. On the other hand, our framework is guaranteed to successfully decouple any collection of parity objectives on strongly-connected graphs, assuming, of course, that they have an intersection. In several graph games, “mixed” or randomised policies are used either out of necessity for winning against the opponent [13] or to reduce the memory requirements of the policies [10]. Our randomised scheduling of local policies can be viewed as randomised policies, where the randomisation over actions is facilitated by the scheduler. However, there is an important difference: usually, randomised policies are designed centrally for the entire objective, whereas our goal is to design isolated local policies independently from the scheduler. The classical distributed view of reactive synthesis [24, 21, 14] uses a fundamentally different model. It is assumed that the actions chosen by each local policy affect a separate set of variables, so that all local policies can be deployed in parallel. In other words, classical distribution synthesis does not require scheduling of policies, and asks how to design local policies whose parallel composition fulfills all objectives. 2 Preliminaries We use ℕN to denote the set of natural numbers 0,1,2,…\0,1,2,…\. For two natural numbers i,ji,j with i<ji<j, we use [i;j][i;j] to denote the set i,i+1,…,j\i,i+1,…,j\ consisting of natural numbers that are at least i and at most j. Sometimes, for a natural number i, we use [i][i] to denote the set [1;i][1;i]. Graphs, and paths. A graph is an ordered triple =(V,E,v)G=(V,E,v_ init), where V is a finite set of vertices, E⊆V×VE V× V is a set of directed edges, and v∈Vv_ init∈ V is the initial vertex. A path in G is a (finite or infinite) sequence of vertices v0v1…v_0v_1… such that v0=v_0=v_ init and (vi,vi+1)∈E(v_i,v_i+1)∈ E for every valid index i. We write ℎ()Paths_ fin(G) and ℎ()Paths_ inf(G) for the sets of finite and infinite paths of G, respectively. By convention, ℎ()Paths_ fin(G) includes the path of length 0. Objectives. An objective φ in G is a set of infinite paths in G. We represent objectives defined using predicates over the vertices of the given graph. We consider the following families of objectives. Reachability. is specified by a set of target vertices T⊆VT V, and is the set of every path that eventually visits at least one vertex in T. Safety. is specified by a set of safe vertices S⊆VS V, and is the set of every path always remaining within the vertices in S. Parity. is specified by a colouring function κ:V↦ℕκ:V , which associates each vertex a natural number called its colour. An infinite path is in the parity objective iff the largest colour that appears infinitely often is even. Büchi. is a special case of parity in which vertices are only coloured by 11 and 22, where the latter are called Büchi vertices. A path is in the Büchi objective iff Büchi vertices are visited infinitely often. Co-Büchi. is a special case of parity in which vertices are only coloured by 0 and 11, where the latter are called co-Büchi vertices or “bad” vertices. A path is in the co-Büchi objective iff it visits co-Büchi vertices only finitely often. We will divide objectives into two complementary families, namely safety and liveness, defined below. While safety can be defined using safe vertices as above, the following definition uses an alternate, semantic variant. Definition 1(Safety versus liveness objectives) Let G be a given graph. A given objective φ in G is called liveness if every finite path in G can be extended into an infinite path in φ . Dually, a given objective φ in G is called safety if every infinite path v0v1…∉φv_0v_1…∉ has a finite prefix ρ=v0…viρ=v_0… v_i such that for every j≥ij≥ i, all infinite extensions of the path v0…vjv_0… v_j is not in φ . Almost-sure satisfaction. Let (V)D(V) denote the set of all probability distributions over V, and given d∈(V)d (V), we will write (d) Supp(d) to denote the support of d. Consider a function f:ℎ()→(V)f:Paths_ fin(G) (V) that, given a finite path ρ ending at a vertex v, assigns a probability distribution whose support is contained in the set of successors of v. We extend f to infinite paths as follows. For a finite path ρ=v0…vkρ=v_0… v_k, the cylinder set spanned by ρ, denoted Cyl(ρ)Cyl(ρ), is the set of all infinite paths whose prefix is ρ. Define the probability distribution over cylinder sets based on f as Prf(Cyl(ρ))=∏i=0k−1f(v0…vi)(vi+1)Pr^f(Cyl(ρ))= _i=0^k-1f(v_0… v_i)(v_i+1). The function PrfPr^f is a pre-measure over the set ℎ()Paths_ inf(G), which extends to a unique probability measure over ℎ()Paths_ inf(G) by applying the Carathéodory’s extension theorem [7]. For simplicity, we use the notation PrfPr^f to also represent the probability measure. We say that f almost surely satisfies an objective φ if Prf(φ)=1Pr^f( )=1. 3 The Decoupled Planning Framework We develop a decoupled framework for generating a path that satisfies a collection φ1,…,φN _1,…, _N of objectives. The framework has two main ingredients, N individual agents and a scheduler. Each Agent i, for i∈[1;N]i∈[1;N], is solely interested in fulfilling the objective φi _i. To this end, the Agent i chooses a policy πi _i, and the policies of all agents are composed at runtime by the scheduler. This section is devoted to formalizing this framework. We start with schedulers. Definition 2(Schedulers: general, fair, deterministic) A scheduler over [N][N] is a function σ:[N]∗→([N])σ:[N]^* ([N]). The scheduler σ is called fair if there exists ϵ>0ε>0 such that for every u∈[N]∗u∈[N]^* and for every n∈[N]n∈[N], Pr(n=σ(u))>ϵPr(n=σ(u))>ε. A scheduler is called deterministic if it always chooses Dirac distributions. We reiterate the advantages of stochastic schedulers mentioned in the introduction. First, they are completely agnostic of the underlying graph and the objectives, while not obstructing policies to fulfill their objectives. Moreover, stochastic schedulers are lightweight and easy to implement. In fact such schedulers are often used in concurrent programs, where multiple programs (analogous to our policies) that are competing for a resource (being scheduled, analogous to our policies being able to execute their actions) are allocated the resource randomly. Henceforth, schedulers will by default be stochastic. Semantics of schedulers. Every sequence from [N]∗∪[N]ω[N]^*∪[N]^ω is called a schedule which is either finite or infinite. Every scheduler σ induces a probability measure over the infinite schedules as follows. Given a finite sequence θ=p0…pk∈[N]∗θ=p_0… p_k∈[N]^*, we define Prσ(Cyl(θ))=∏i=0k−1σ(p0…pk−1)Pr^σ(Cyl(θ))= _i=0^k-1σ(p_0… p_k-1), which is a pre-measure that extends to a unique measure—also denoted as PrσPr^σ—over the set [N]ω[N]^ω by applying Carathéodory’s extension theorem [7].∎ We formalize the second ingredient of our framework, the policies that the agents choose, where we define policy types with increasing knowledge of scheduling choices. We introduce some notation first. Given two alphabets A and B, and a pair of finite words of equal length wA=a0…ak∈A∗w_A=a_0… a_k∈ A^* and wB=b0…bk∈B∗w_B=b_0… b_k∈ B^*, we define their element-wise cross-product as: wA⊗wB≔(a0,b0)…(ak,bk)∈(A×B)∗w_A w_B (a_0,b_0)…(a_k,b_k)∈(A× B)^*. Furthermore, we lift this cross-product to sets of sequences: given WA⊆A∗W_A A^* and WB⊆B∗W_B B^*, define WA⊗WB≔W_A W_B wA⊗wB∣wA∈\w_A w_B w_A∈ WA,wB∈WBW_A,w_B∈ W_B\. Definition 3(Policies augmented with scheduling information) Let σ be a scheduler over [N][N]. Path-aware. policies coincide with the traditional definition of policies and have no scheduling knowledge, they are of the form π:ℎ()→(V)π _ fin(G) (V). We denote the set of path-aware policies by ΠPath ^Path. Scheduled-aware. policies keep track of which past time points they have been scheduled, and all choices made by it in the past. A scheduled-aware policy is a partial function of the form π:ℎ()⊗⊤,⊥∗⊗V∗→(V)π _ fin(G) \ , \^* V^* (V), mapping the path ρ=v0…vk∈ℎ()ρ=v_0… v_k _ fin(G), the history θ=q0…qk−1∈⊤,⊥∗θ=q_0… q_k-1∈ \ , \^* of time points in which it was scheduled, where “⊤ ” means “scheduled” and “⊥ ” means not scheduled, and the history of choices γ=w1…wk∈V∗γ=w_1… w_k∈ V^* made by it, to the distribution π(ρ,θ,γ)π(ρ,θ,γ). The distribution π(ρ,θ,γ)π(ρ,θ,γ) is defined iff ρ, θ, and γ are consistent, i.e., for every i∈[k]i∈[k] with qi−1=⊤q_i-1= , vi=wiv_i=w_i. The set of all full scheduled-aware policies will be denoted as ΠS ^S. Full history-aware. policies enrich scheduled-aware policies by additionally including the indices of scheduled agents during times it was unscheduled (instead of just keeping track of “⊥ ” as scheduled-aware policies do). Without loss of generality, assume that the indices of the other policies are [2;N][2;N]. A full history-aware policy is a partial functions of the form π:ℎ()⊗⊤,2,…,N∗⊗V∗→(V)π _ fin(G) \ ,2,…,N \^* V^* (V), mapping the path ρ∈ℎ()ρ _ fin(G), the history of scheduling decisions θ∈⊤,2,…,N∗θ∈ \ ,2,…,N \^*, and the history of choices γ∈V∗γ∈ V^* made by π, to the distribution π(ρ,θ,γ)π(ρ,θ,γ). The distribution π(ρ,θ,γ)π(ρ,θ,γ) is defined under the same conditions as for scheduled-aware policies. The set of all full history-aware policies with N agents will be denoted as ΠNFH ^FH_N. For each policy, regardless of its type, for every given path ρv∈ℎ()ρ v _ fin(G), the support of the output distribution over vertices must be a subset of (v) Supp(v). Remark 1(Why keep track of past choices?) One may naïvely think that it is redundant that policies in ΠS ^S and ΠNFH ^FH_N keep track of their own past choices, alongside the whole path history, because the old histories could be used to simulate the old choices on demand. This will not work since the policies are stochastic, and executing them on the same history will generate different outcomes on different instances with positive probability. Remark 2(Comparing decoupling strength) Decoupling is stronger when using a family of policies with weaker scheduling information. Since path-aware policies coincide with the traditional definition of policies, an agent can use any off-the-shelf tool to construct a policy for their objective. This is no longer the case with scheduled-aware and full history-aware policies. Yet, an appealing feature of scheduled-aware policies is their independence of how many policies are interacting. This enables, for example, “patching” a deployed system by removing or adding an objective at runtime. Indeed, even when N changes, no update is needed to an individual policy. This is no longer the case with full history-aware policies. We point out that decoupling with full history-aware policies still provides modularity: as long as the number of objectives is fixed, changes to objectives at runtime is possible by changing only the relevant policies. We define the composition of a scheduler and a collection of full history-aware policies. This generates a probability distribution over the infinite paths generated by a random interleaving of the individual local policies. Definition 4(Composition) Suppose we are given a graph G, a scheduler σ for a set of N agents, and a set of policies π1,…,πN _1,…, _N where for every i∈[N]i∈[N], πi∈ΠNFH∪ΠS∪ΠPath _i∈ ^FH_N∪ ^S∪ ^Path. The composition is the tuple ℐ=(,πi,…,πN,σ)I=(G, _i,…, _N,σ). Each composition defines a probability distribution over the paths generated, which we computed step-by-step below. Such a distribution depends on the type of scheduler, hence we define it carefully below. Semantics of composition. At each time point i, when the current path is v0…vi∈ℎ()v_0… v_i _ fin(G), each Agent j randomly selects the next vertex wi+1jw_i+1^j using its policy, giving us a tuple (wi+11,…,wi+1N)(w_i+1^1,…,w_i+1^N) of selections. Out of this tuple, the choice of the scheduled agent pip_i is used to extend the current path to v0…vi+1v_0… v_i+1, where vi+1=wi+1piv_i+1=w_i+1^p_i, and the process continues. For a given fixed schedule p0…pk−1∈[N]∗p_0… p_k-1∈[N]^*, we define the probability of the sequence of selections being (w11,…,w1N)…(wk1,…,wkN)(w_1^1,…,w_1^N)…(w_k^1,…,w_k^N) given as: Prℐ((w11,…,w1N)…(wk1,…,wkN)∣(p0,…pk−1))≔∏j=1N∏i=0k−1D(wi+1j), ^I ((w_1^1,…,w_1^N)…(w_k^1,…,w_k^N) (p_0,… p_k-1) ) _j=1^N _i=0^k-1D(w_i+1^j), (1) where D(wi+1j)D(w_i+1^j) represents the probability that at time i+1i+1, the policy πj _j selected the vertex wi+1jw_i+1^j, whose value is defined based on the policy type as below. In the above, the path generated by the schedule p0,…pk−1p_0,… p_k-1 from the sequence (w11,…,w1N)…(wk1,…,wkN)(w_1^1,…,w_1^N)…(w_k^1,…,w_k^N) is v0v1…vkv_0v_1… v_k where v0=v_0=v_ init and for each i∈[k]i∈[k], vi=wipi−1v_i=w_i^p_i-1. The set of all policies are πjj∈[N] \ _j \_j∈[N]. Then, D(wi+1j)=πj(v0,…vi)πj∈ΠPath,πj((v0…vi),(q0…qi−1),(w1j…wij)),∀t.qt=⊤⇔pt=jπj∈ΠS,πj((v0…vi),(p0…pi−1),(w1j…wij))πj∈ΠNFH.D(w_i+1^j)=\\ cases _j (v_0,… v_i )& _j∈ ^Path,\\ _j ((v_0… v_i),(q_0… q_i-1),(w_1^j… w_i^j) ),\,∀ t\;.\;q_t= p_t=j& _j∈ ^S,\\ _j ((v_0… v_i),(p_0… p_i-1),(w_1^j… w_i^j) )& _j∈ ^FH_N. cases Suppose we are given a finite path ρ=v0…vk∈ℎ()ρ=v_0… v_k _ fin(G) and a schedule θ=p0…pk−1∈[N]∗θ=p_0… p_k-1∈[N]^*. We introduce the set Σv0,ρ,θ⊆VN×k _v_0,ρ,θ V^N× k representing the set of all sequences of vertices generated by all agents such that the schedule θ would produce the path ρ starting at the initial vertex v0v_0. Formally, Σv0,ρ,θ≔(v11,…,v1N)…(vk1,…,vkN)∣∀i∈[k].vi=vipi−1 _v_0,ρ,θ \(v_1^1,…,v_1^N)…(v_k^1,…,v_k^N) ∀ i∈[k]\;.\;v_i=v_i^p_i-1 \. Now we combine Prℐ(ρ∣⋅)Pr^I(ρ ·) with the probability measure PrσPr^σ over sequences of policy indices, and write Prℐ(Cyl(ρ))Pr^I(Cyl(ρ)) as ∑θ∈[N]k−1(v11,…,v1N)…(vk1,…,vkN)∈Σv0,ρ,θPrℐ((v11,…,v1N)…(vk1,…,vkN)∣θ)⋅Prσ(θ), _ subarraycθ∈[N]^k-1\\ (v_1^1,…,v_1^N)…(v_k^1,…,v_k^N)∈ _v_0,ρ,θ subarrayPr^I((v_1^1,…,v_1^N)…(v_k^1,…,v_k^N) θ)·Pr^σ(θ), (2) which is a pre-measure and leads to a unique measure—also written PrℐPr^I—over the set of all infinite paths by applying the Carathéodory’s extension theorem [7]. We will write ℐ⊧..φI _ a.s.\! iff Prℐ(φ)=1Pr^I( )=1.∎ Following is the decoupling problem that we undertake. Problem statement (informal): decoupled planning Fix a fair, stochastic scheduler σ. Suppose G is a given graph and φ1,…,φN _1,…, _N are the objectives. Independently design the policies π1,…,πN _1,…, _N in a way that ℐ(,π1,…,πN,σ)⊧..φ1∧…∧φNI(G, _1,…, _N,σ) _ a.s.\! _1 … _N. Towards this goal, we start by stating why a fair deterministic scheduler would not suffice in achieving the desired decoupling, which formalizes the informal description in Example 1. restatable [No deterministic scheduler can be universal]theoremNoDetSched For every deterministic scheduler σ, there exist a graph G and reachability objectives φ1 _1 and φ2 _2 with (φ1∩φ2)≠∅( _1∩ _2)≠ and deterministic policies π1σπ^σ_1 and π2σπ^σ_2 that respectively satisfy φ1 _1 and φ2 _2, but (,π1σ,π2σ,σ)⊧̸φ1∧φ2(G, _1^σ, _2^σ,σ) _1 _2. The high level idea (slightly over-simplified) of the proof appears in Example 1, and a rigorous proof can be found Appendix 0.A.1. This limitation of (extremely) fair deterministic schedulers inspired us to use stochastic schedulers with the stronger probabilistic fairness [12] properties. 4 Building Support for Safety Components of ω-Regular Objectives We start by demonstrating the challenge of incorporating safety. vva2a_2a1a_1 Figure 2: A graph with a safety objective G(¬a1)G( a_1) and a Büchi objective GFa2GFa_2. Example 5 Consider the graph depicted in Figure 2, and two objectives, the safety objective φ1 _1 requires “avoid the Red vertex a1a_1” and a Büchi objective φ2 _2 requires “visit the Blue vertex a2a_2 infinitely often”. Suppose that Agent 22 chooses the policy π2 _2 that alternates between selecting a1a_1 and a2a_2 at v. Note that if π2 _2 is always scheduled, then φ2 _2 is satisfied. Observe that no matter which policy Agent 11 chooses, any stochastic scheduler that schedules π2 _2 at v with probability at least ϵ>0ε>0 leads to a random walk that visits a1a_1 almost surely and thus violates φ1 _1. Finally, note that the path (v,a1)ω(v,a_1)^ω satisfies φ1∧φ2 _1 _2. ∎ As demonstrated in Examples 1 and 4, liveness objectives allow for flexible decoupling. Safety, however, is rigid. Indeed, it is well known that almost-sure and sure satisfaction coincide for safety [13]. That is, in order to satisfy safety, a composition needs to satisfy it deterministically on every path. This requires communication, which we establish by augmenting the policies with a safety-preserving component defined as follows. Maximally permissive policies. A maximally permissive policy for a safety specification φ is χ:V→2Vχ:V→ 2^V. Intuitively, for a vertex v, the set χ(v)χ(v) represents safe continuations from v. More formally, a path ρ=v0,v1,…ρ=v_0,v_1,… such that vi+1∈χ(vi)v_i+1∈χ(v_i) satisfies φ . Maximality of χ means that for every v and every u∉χ(v)u∉χ(v), there is a continuation from u that violates φ . In order to construct χ, we compute the set of vertices from which φi _i can be fulfilled, which we call the winning region and denote it by W. Then, for every v∈Wv∈ W, we define χ(v)=u:E(v,u)∧u∈Wχ(v)= \u:E(v,u) u∈ W \. Observe that χ is maximal; proceeding to u∉χ(v)u∉χ(v) violates φ . Shielded composition. We augment the composition defined in Def. 4 with maximally-permissive policies. Consider policies π1,…,πN _1,…, _N and maximally-permissive policies χ1,…,χN _1,…, _N. Whenever Agent i∈[N]i∈[N] is scheduled at vertex v, every other Agent j≠ij≠ i sends χj(v) _j(v) to Agent i. Agent i selects a vertex πi(v)∈⋂1≤j≤Nχj(v) _i(v)∈ _1≤ j≤ N _j(v) that is safe for all. We will prove that, under mild conditions on the graph and objectives, there is always such a safe vertex to choose. Decomposition of ω-regular specifications. Consider an ω-regular objective φi _i for Agent i. It is possible to decompose φi _i into a safety and a liveness component φi safe_i and φi live_i, such that φi=φi∩φi _i= safe_i∩ live_i [1]. Let WiW_i be the maximal winning region, WicW_i^c the complement of WiW_i, and ℎ(Wic)Reach(W_i^c) the objective that contains all paths eventually reaching WicW_i^c. Define φi≔φi∪ℎ(Wic) live_i _i (W_i^c). Observe that φi live_i is a liveness objective, since no matter what prefix we have seen, we can either stay in WiW_i and fulfil φi _i, or reach WicW_i^c. Clearly φi=φi∩φi _i= safe_i∩ live_i, and moreover, φi live_i can be expressed as a parity objective (possibly with additional colours). We describe how the agents act. Let πi _i be a policy for Agent i and let χi _i be a maximally permissive policy. As before, when Agent i is scheduled following path ρ that ends at v, every other Agent j sends χj(v) _j(v) and Agent i selects πi(ρ)∈⋂jχj(v) _i(ρ)∈ _j _j(v). We call this a shielded composition, and denote it by (,π1,…,πn,σ)(G, _1,…, _n,σ) shld. We omit the maximally permissive policies for brevity. Mutual safety closed. Consider an objective φ⊆Vω V^ω, we define (φ)≔u∈V⋆∣∃v∈Vω.uv∈φPref( ) \u∈ V ∃ v∈ V^ω\;.\;uv∈ \ to be the set of all finite prefixes of φ . We call a pair of objectives φ1 _1 and φ2 _2 mutually safety-closed, if every path $in$G fulfilling (φ_1)∩(φ_2)$alsofulfils$(φ_1∩φ_2)$.Bytransitivity,wecangeneralizemutualsafety−closuretoarbitrarynumberofobjectives.Themutuallysafetyclosedassumptionguaranteesthateveryprefixofapathhasanextensionthatsatisfieseachobjective.Thisensuresthatapaththatmakesa‘wrongstep′canalwaysrecover.111Assumption 1The objectives $φ_1,…,φ_N$ are mutually safety-closed.Let$W_i$bethemaximalsetofverticesin$$fromwhichtheagent$i$hasapolicytofulfil$φ_i$.Inotherwords,$φ_i=(W_i)$.Define$W≔∩_i∈[N]W_i$.Byassumption,$W$isnonempty,since$v∈W_i$forall$i$.Let$[W]$bethesubgraphobtainedbyremovingallthevertices$V∖W$from$$,andbyremovingalltheedgesthatinvolvethesevertices.IfAssumption˜1holds,thenitcanbeshownthatthesubgraph$[W]$isdeadlock−free(seeProp.˜1inAppendix˜0.B),andthereforeeverypathcanbeextendedintoaninfinitepath.Wearenowreadytopresentthemaintheoremofthissection(seeitsproofinAppendix˜0.B),whichsuggeststhefollowingdecouplingframeworkfor$ω$−regularobjectives.Theshieldedcompositionthatisdescribedabovekeepsthepathinthestrongly-connectedregion$G[W]$thatissafeforallagents.Thisleavesuswithliveness,whichthepolicies$π_1,…,π_N$takecareof.Constructing$π_1,…,π_N$isnottrivial.Insubsequentsections,wedevelopsuchconstructions%onlyfocusontheleftsideoftheimplicationinEqn.˜4,whileassumingthatthegraphisstronglyconnectedandallobjectivesarelivenessobjectives.restatable[Compositionalenforcementofthesafetycomponents]theoremsafetyclosedSupposeAssumption˜1holdstrue.Thenforeveryfairscheduler$σ$andeverysetoflocalpolicies$π_1,…,π_N$thefollowingholds:%[([W],π_1,…,π_N,σ)⊧..⋂_i=1ˆNφ_i]⟹[(,π_1,…,π_N,σ)ˆ⊧..⋂_i=1ˆNφ_i].%%InlightofTheorem˜4,fromthispointonward,weonlyfocusontheleftsideoftheimplicationinEqn.˜4,andassumethatthegivengraphisstronglyconnectedandallobjectivesarelivenessobjectives.%KM:Adjustthedefinitionsofthesetermsinthepreliminaries. ∈ ( \_1) ( \_2)$alsofulfils$ ∈ ( \_1∩ \_2)$.Bytransitivity,wecangeneralizemutualsafety-closuretoarbitrarynumberofobjectives. Themutuallysafetyclosedassumptionguaranteesthateveryprefixofapathhasanextensionthatsatisfieseachobjective.Thisensuresthatapaththatmakesa``wrongstep canalwaysrecover. assumptionThe objectives $ \ _1,…, _N \$ are mutually safety-closed. assumption Let$W\_i$bethemaximalsetofverticesin$G$fromwhichtheagent$i$hasapolicytofulfil$ \_i$.Inotherwords,$ safe\_i=Safe(W\_i)$.Define$W ∩\_i∈[N]W\_i$.Byassumption,$W$isnonempty,since$v_ init∈ W\_i$forall$i$.Let$G[W]$bethesubgraphobtainedbyremovingallthevertices$V W$from$G$,andbyremovingalltheedgesthatinvolvethesevertices.IfAssumption~ assuump:safetty closureholds,thenitcanbeshownthatthesubgraph$G[W]$isdeadlock-free(seeProp.~ Prop:subgraph is dead end freeinAppendix~ appn: safety),andthereforeeverypathcanbeextendedintoaninfinitepath. Wearenowreadytopresentthemaintheoremofthissection(seeitsproofinAppendix~ appn: safety),whichsuggeststhefollowingdecouplingframeworkfor$ω$-regularobjectives.Theshieldedcompositionthatisdescribedabovekeepsthepathinthe strongly-connectedregion$G[W]$thatissafeforallagents.Thisleavesuswithliveness,whichthepolicies$π\_1,…,π\_N$takecareof.Constructing$π\_1,…,π\_N$isnottrivial.Insubsequentsections,wedevelopsuchconstructions%onlyfocusontheleftsideoftheimplicationinEqn.~ eq:safeety liveness,whileassumingthatthegraphisstronglyconnectedandallobjectivesarelivenessobjectives. [Compositionalenforcementofthesafetycomponents]theoremsafetyclosedSupposeAssumption~ assuump:safetty closureholdstrue.Thenforeveryfairscheduler$σ$andeverysetoflocalpolicies$π\_1,…,π\_N$thefollowingholds: aligned % [(G[W],π\_1,…,π\_N,σ) _ a.s.\! \_i=1^N live\_i ] [(G,π\_1,…,π\_N,σ) shld _ a.s.\! \_i=1^N \_i ]. aligned % [rgb]0,0.5,0 [named]pgfstrokecolorrgb0,0.5,0%InlightofTheorem~ thm:safetyclosed,fromthispointonward,weonlyfocusontheleftsideoftheimplicationinEqn.~ eq:safeety liveness,andassumethatthegivengraphisstronglyconnectedandallobjectivesarelivenessobjectives.% [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0KM:Adjustthedefinitionsofthesetermsinthepreliminaries. 5 Decoupling Liveness Objectives via Conventions Unlike safety objectives, we show that liveness objectives can be decomposed without any direct communications among agents. However, this does not rule out the need for coordination. In fact, already for Büchi objectives on strongly connected graphs, without coordination the agents may not be able to fulfill their objectives. This is somewhat surprising, and the intuition was sketched in Example 2. We formally state this result in the following theorem. restatable [No stochastic scheduler for uncoordinated Büchi policies]theoremNoUnivBuchischeduler There is a graph G such that for any stochastic scheduler σ, there are Büchi objectives φ1 _1 and φ2 _2 with (φ1∩φ2)≠∅( _1∩ _2)≠ and deterministic policies π1σπ^σ_1 and π2σπ^σ_2 that respectively satisfy φ1 _1 and φ2 _2, but the composition (,π1σ,π2σ,σ)⊧̸..φ1∩φ2(G, _1^σ, _2^σ,σ) _ a.s.\! _1∩ _2. We remark that the proof above also shows that even for a reachability objective, despite using Büchi strategies that ensure that every prefix satisfies the Büchi objective, the probability of reaching an accepting state can be bounded by 1/21/2 (union bound). Corollary 1(No stochastic scheduler for uncoordinated reachability objectives) There exists a graph G such that for every scheduler σ, there exists reachability objectives φ1 _1 and φ2 _2 with (φ1∩φ2)≠∅( _1∩ _2)≠ and deterministic policies π1σπ^σ_1 and π2σπ^σ_2 that respectively satisfy φ1 _1 and φ2 _2, but (,π1σ,π2σ,σ)⊧̸..φ1∩φ2(G, _1^σ, _2^σ,σ) _ a.s.\! _1∩ _2. These results motivate us to seek mechanisms that would induce the required coordination among agents, without them requiring to establish direct communication during the design and deployment of their policies. To this end, we formalize conventions, which are rules that agents should follow while selecting their policies, and it is guaranteed if every agent follow these conventions, the composition will fulfill all objectives. Fig. 3 illustrates how conventions are used. Definition 5(Conventions) Consider a family of objectives α, where we focus on α∈Büchi,co-Büchi,parityα∈ \B\"uchi,co-B\"uchi,parity \. A convention ConvαConv_α for the family α is a mapping that takes a graph G, a scheduler σ, and an objective φ , and outputs a collection of policies of type β that the agent can choose from. We focus on β∈Π~NFH,Π~S,Π~Pathβ∈ \ ^FH_N, ^S, ^Path \ and design a convention ConvαConv_α such that for every ,σG,σ, and φ∈α ∈α, we have Convα(,σ,φ)⊆βConv_α(G,σ, ) β. • Soundness: A convention ConvαConv_α is sound for classes of graphs and schedules, if for every graph G and schedule σ from the respective class, and collection of objectives φ1,…,φN∈α _1,…, _N∈α, if for every i∈1,…,Ni∈ \1,…,N \ and πi∈Convα(,σ,φi) _i _α(G,σ, _i), we have (,πi,…,πN,σ)⊧..φ(G, _i,…, _N,σ) _ a.s.\! . • A partial order on conventions: Consider two conventions ConvαConv_α and Convα′Conv _α. We define Convα⪯Convα′Conv_α _α if ConvαConv_α uses policies with weaker scheduling information or if ConvαConv_α is less restrictive than Convα′Conv _α, that is for every ,σ,φG,σ, , we have Convα′(,σ,φ)⊆Convα(,σ,φ)Conv _α(G,σ, ) _α(G,σ, ). Figure 3: Decoupling planning using a convention ConvαConv_α. Observe that ConvαConv_α is independent of the graph, scheduler, or specific objectives. Agent i independently chooses πi∈Convα(,σ,φi) _i _α(G,σ, _i) that agrees with the convention. Soundness of ConvαConv_α implies that the output almost-surely satisfies φ . We now present the problem that we will study. Problem statement: decoupled planning of liveness objectives We focus on strongly-connected graphs and fair stochastic schedulers. For a family of objectives α∈Büchi,co-Büchi,parityα∈ \B\"uchi,co-B\"uchi,parity \. Find a sound and minimal convention ConvαConv_α. Our focus is on finding sound conventions and we do not show optimality, i.e., provide lower bounds to show inexistence of better conventions. We argue that finding conventions that suffice for decoupling is a nontrivial and challenging problem since conventions are fixed before the graph, scheduler, and objectives are known. Moreover, developing conventions has practical applications whereas showing their inexistence does not. 6 Convention for Decoupling Büchi Objectives We show that decoupling is possible for Büchi objectives with mildly restricted path-aware policies; that is, Büchi admits a strong form of decoupling. Definition 6(Policies with uniform bounded hitting-time) Let =(V,E,v0)G=(V,E,v_0) be a graph and let π∈ΠPπ∈ ^P be a stochastic policy on G. Fix a subset B⊆VB V and a finite path α=v0v1…vk∈ℎ()α=v_0v_1… v_k _ fin(G). The hitting time random variable of B under π from α is defined by τπ(α)(ρ):=mint≥1∣vk+t∈B in the extension ρ∈Extπ(α), _π(α)(ρ)\;:=\; \\,t≥ 1 v_k+t∈ B in the extension ρ _π(α)\,\, with the convention τπ(α)(ρ)=∞ _π(α)(ρ)=∞ if no such t exists. The expected hitting time of B from α under π is then π[τπ(α)]=∫Extπ(α)τπ(α)(ρ)Prπ(ρ)E_π[ _π(α)]\;=\; _Ext_π(α) _π(α)(ρ)\,dPr^π(ρ). We say that π has uniformly bounded expected hitting time for B if there exists a finite constant L such that supα∈ℎ()π[τπ(α)]≤L _α _ fin(G)E_π[ _π(α)]\;≤\;L. The following theorem proves implementation of any such policies with a stochastic scheduler is good for all. The proof can be found in Appendix 0.C. restatable theoremdenseUniformBuchi Consider a strongly connected graph G, policies π1,…,πN _1,…, _N with uniform bounded hitting-time for Büchi objectives φ1,…,φN _1,…, _N, and a stochastic scheduler σ. Then, (,π1,…,πN,σ)⊧..⋂1≤i≤Nφi(G, _1,…, _N,σ) _ a.s.\! _1≤ i≤ N _i. 7 Convention for Decoupling Co-Büchi Objectives We start by showing that restricting to dense path aware policies does not suffice for co-Büchi objectives. restatabletheoremNoUnivCoBuchi There is a graph, two co-Büchi objectives φ1 _1 and φ2 _2 with (φ1∩φ2)≠∅( _1∩ _2)≠ and deterministic memoryless policies π1σπ^σ_1 and π2σπ^σ_2 that respectively satisfy φ1 _1 and φ2 _2, but for any scheduler σ, we have (,π1σ,π2σ,σ)⊧̸..φ1∩φ2(G, _1^σ, _2^σ,σ) _ a.s.\! _1∩ _2. Proof(sketch) Consider the graph G depicted in Fig.˜4. For i∈1,2i∈ \1,2 \, the “bad” co-Büchi vertex for objective φi _i is v1iv_1i. Note that (φ1∩φ2)≠∅( _1∩ _2)≠ since v0ωv_0^ω satisfies both objectives. We define πi(v1)=v1,i _i(v_1)=v_1,i, otherwise the policies are identical. Observe that πi _i satisfies φi _i. However, for any stochastic scheduler, all vertices will be almost-surely visited, which violates both objectives. The proof can be found in App. 0.D.1. v0v_0v1v_1v1,1v_1,1v1,2v_1,2 Figure 4: A graph with two co-Büchi objectives given by bad states v1,1v_1,1 ( Red) and v1,2v_1,2 ( Blue). Red edges are chosen by π1 _1 and Blue edges by π2 _2. 7.1 A convention for co-Büchi objectives Consider a strongly-connected graph G, a stochastic scheduler σ, and a co-Büchi objective φ given by a set of “bad” states B. Let ℭB C_B denote the set of “good” simple cycles in G that are disjoint from B. A policy π∈Convco-Büchi(,σ,φ)π _co-B\"uchi(G,σ, ) proceeds as follows. It randomly chooses a lasso path ρ⋅Cωρ· C^ω, where ρ is a simple path and C∈ℭBC∈ C_B. If π is scheduled in a turn, if C has not yet been reached, it chooses the next vertex on ρ, and otherwise advances on C. Suppose that π is not scheduled, and let π′π be the scheduled policy. Let v be the vertex that π would have chosen if it was scheduled and let v′v be the vertex that π′π chooses. If v=v′v=v , we proceed to the next turn. If v≠v′v≠ v , then π′π realizes it is in conflict with π: the lasso that π chose differs from the choice of π′π . Then, π′π randomly chooses a different lasso path ρ′⋅C′ωρ · C ω with C′∈ℭBC ∈ C_B. Correctness will be derived from the property of co-Büchi objectives that if there is a path that satisfies all objectives, then there is a lasso ρ⋅Cωρ· C^ω with C∈ℭBC∈ C_B that is good for all. The idea is that almost surely, all policies will eventually choose the same lasso path leading to the generated path “stabilizing” on a cycle that is good for all. We describe π formally. The memory states of π are M=ℎ()×ℭBM=Paths_ fin(G)× C_B, where a state ⟨ρ,C⟩∈M ρ,C ∈ M means that π chooses cycle C and the path ρ leading to it. The interaction with a scheduler and the other policies generates a random sequence, and π’s local view of the sequence is ⟨m0,v0⟩,⟨m1,v1⟩,… m_0,v_0 , m_1,v_1 ,…, where for i≥0i≥ 0, each mi=⟨ηi,Ci⟩∈Mm_i= _i,C_i ∈ M is a memory state and vi∈Vv_i∈ V is a location on G. The policy maintains the invariant that the location in G matches the first vertex of η, namely ηi[0]=vi _i[0]=v_i. We use ⊤ and ⊥ to respectively denote that π is and is not scheduled. The definition of ⟨mi+1,vi+1⟩=π(mi,vi,⊤) m_i+1,v_i+1 =π(m_i,v_i, ) is deterministic and depends on whether the cycle has been reached: (1) CiC_i has not been reached: then we define vi+1=η[1]v_i+1=η[1] and mi+1=⟨η[1:],Ci⟩m_i+1= η[1:],C_i , and (2) CiC_i has been reached: then ηi=ϵ _i=ε and we define mi+1=mim_i+1=m_i and vi+1v_i+1 is the successor of viv_i on C. We proceed to define π(mi,vi,⊥)π(m_i,v_i, ). Let ⟨m,v⟩=π(mi,vi,⊤) m,v =π(m_i,v_i, ) be π’s choice if it was scheduled, and let vi+1v_i+1 be the vertex chosen by some other policy. If v=vi+1v=v_i+1, then the update is as above, mi+1=m_i+1=m. If vi+1≠v_i+1≠ v, then π randomly selects Ci+1∈ℭBC_i+1∈ C_B and a simple path ηi+1 _i+1 from vi+1v_i+1 to Ci+1C_i+1. To prove the following theorem, we construct a Markov chain that simulates the global state of the policies and show that its Bottom Strongly Connected Components (BSCCs) are states in which the policies are in consensus regarding the choice of a lasso path that is good for all. The proof then follows from the property of Markov chains that a random walk reaches a BSCC almost surely. The full proof is available in Appendix 0.D.2. restatable theoremcoBuchischeduling Let B1,…,BNB_1,…,B_N be a collection of co-Büchi objectives on a graph G. For every choice of policies that satisfies the co-Büchi condition πi∈χBi _i∈ _B_i, for i∈[N]i∈[N], and a fair scheduler σ, we have (,π1,…,πN,σ)⊧..⋀1≤i≤Nφi(G, _1,…, _N,σ) _ a.s.\! _1≤ i≤ N _i. 8 Convention for Decoupling Parity Objectives We generalize the ideas for decoupling co-Büchi objectives to parity objectives. The construction requires full-history aware policies when N>2N>2. Fix a graph G and stochastic scheduler σ. The co-Büchi convention relies on the property that if there is a path that satisfies all objectives, there is such a lasso path. This is no longer the case for parity objectives. For example, consider the graph depicted in Fig. 1(a) and objectives φ1=(GFℓ)∧(G¬b1) _1=(GF ) (G b_1) and φ2=(GFr)∧(G¬b1) _2=(GFr) (G b_1), then a path that satisfies both must cycle between r and ℓ via t1t_1 and t2t_2. This is not a simple cycle since both outgoing edges of t1t_1 and t2t_2 are traversed infinitely often. We overcome this using the following lemma whose proof can be found in App. 0.E.1. Lemma 1 Consider parity objectives κ1,…,κN:V→ℕ _1,…, _N:V with ⋀i∈[1;N]κi≠∅ _i∈[1;N] _i≠ . Then, there are memoryless policies ⟨θ1,…,θN⟩:V→V _1,…, _N :V→ V such that (,θ1,…,θN(G, _1,…, _N, σ)⊧..⋀i∈[1;N]κiσ) _ a.s.\! _i∈[1;N] _i For example, Fig. 1(a) depicts two memoryless policies π1 _1 and π2 _2 for which we have (,π1,π2,σ)⊧..φ1∧φ2(G, _1, _2,σ) _ a.s.\! _1 _2 since the generated random walk almost surely visits each of the vertices ℓ,t1,t2,r ,t_1,t_2,r infinitely often. Parity convention. Consider a parity objective given by a colouring function κi:V→ℕ _i:V . A policy πi∈ConvParity(,σ,κ) _i _Parity(G,σ,κ) randomly chooses an N-tuple of internal memoryless policies θ1,…θN _1,… _N such that (,θ1,…θN,σ)⊧..κi(G, _1,… _N,σ) _ a.s.\! _i. Intuitively, when scheduled, πi _i follows θi _i, and θj _j, for j≠ij≠ i, constitutes a guess of the internal policy that πj _j follows. At vertex v, if πi _i is scheduled, it proceed to θi(v) _i(v) and if πj _j is scheduled and chooses u≠θi(v)u≠ _i(v), then πi _i observes a conflict and randomly chooses a new N-tuple of internal memoryless policies. In order to observe a conflict, πi _i requires knowledge of who is scheduled and their choice, thus it is a full-history aware policy. We describe πi _i formally. Its memory states are M=(V)NM=(V^V)^N. The interaction with a scheduler and the other policies generates a random sequence, and πi _i’s local view of the sequence is ⟨m0,v0⟩,⟨m1,v1⟩,… m_0,v_0 , m_1,v_1 ,…, where at time j≥0j≥ 0, the location in G is vj∈Vv_j∈ V and the memory state is mj=⟨θj,1,…θj,N⟩∈Mm_j= _j,1,… _j,N ∈ M. If πi _i is scheduled at time j, we define vj+1=θj,i(vj)v_j+1= _j,i(v_j) and the memory state is unchanged, namely mj+1=mjm_j+1=m_j. Suppose that πi′ _i is scheduled and chooses u, then we define u=vj+1u=v_j+1. If u=θj,i(vj)u= _j,i(v_j), then there is no conflict and mj+1=mjm_j+1=m_j. Otherwise, u≠θj,i(vj)u≠ _j,i(v_j), policy πi _i realizes a conflict and randomly chooses mj+1=⟨θj+1,1,…θj+1,N⟩∈Mm_j+1= _j+1,1,… _j+1,N ∈ M. The following theorem is obtained by reasoning about the Markov chain that simulates the global state of the policies, carefully identifying consensus global states that are trivially good for all, and showing that they form the BSSCs of the Markov chain. The proof is available in Appendix 0.E.2. restatable theoremparityscheduling Consider a strongly-connected graph G, a stochastic scheduler σ, and a collection of N parity objectives κ1,…,κN _1,…, _N having ⋂1≤i≤Nκi≠∅ _1≤ i≤ N _i≠ . For every collection of policies π1,…,πN _1,…, _N that satisfy the convention, i.e., πi∈Convparity(,σ,κi) _i _parity(G,σ, _i), for i∈1,…,Ni∈ \1,…,N \, we have (,π1,…,πN,σ)⊧..⋀1≤i≤Nκi(G, _1,…, _N,σ) _ a.s.\! _1≤ i≤ N _i. 9 Discussion We established sufficient conditions under which local policies for different ω-regular objectives can be composed under a common scheduler to almost-surely satisfy all objectives, showing that Büchi, co-Büchi, and parity objectives require progressively richer scheduler awareness. Although our focus is on multi-parity objectives, the framework and the existence results for universal local policies naturally extend to any class of specifications implementable via finite-memory strategies, provided the memory bound is common knowledge among all modules. In this setting, each module may guess a finite-memory strategy per agent (rather than a memoryless one) whose bounded memory size is shared across modules. Interestingly, while our analysis in Section˜8 shows that full-history awareness is necessary in general, there are special cases that require less information. For instance, when there are only two agents with parity objectives, each can infer the scheduler’s choice from the observed transition: if the transition corresponds to its own proposed action, the agent was scheduled; otherwise, the other agent was. Hence, no explicit communication from the scheduler is needed in this case. For parity objectives, the memory size of each agent typically scales with the number of agents, as each agent must maintain a guess of a cycle for every other agent (including itself). However, if an agent has additional knowledge—e.g., that some others have Büchi or co-Büchi objectives—this requirement can be reduced. When a parity objective is combined with a (co-)Büchi objective, satisfiability can be achieved via a single simple cycle, eliminating the need for additional memory components. Although we establish the existence of such universal schedulers, our work does not address their convergence properties. In particular, the expected convergence time of the presented protocol is likely to be exponential in the size of the underlying system. Improving this convergence time remains is not discussed in this paper. We conjecture that techniques from reinforcement learning or stochastic approximation could be adapted to accelerate convergence while preserving correctness guarantees, and is left for future work. References [1] Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed computing 2(3), 117–126 (1987) [2] Anand, A., Nayak, S.P., Schmuck, A.K.: Synthesizing permissive winning strategy templates for parity games. In: International Conference on Computer Aided Verification. p. 436–458. Springer (2023) [3] Avni, G., Henzinger, T.A., Chonev, V.: Infinite-duration bidding games. J. ACM 66(4), 31:1–31:29 (2019) [4] Avni, G., Mallik, K., Sadhukhan, S.: Auction-based scheduling. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. p. 153–172. Springer (2024) [5] Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. p. 256–271. Springer (2015) [6] Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives. Information and Computation 261, 536–587 (2018) [7] Billingsley, P.: Probability and Measure. Wiley, New York, 3rd edn. (1995) [8] Borel, É.: Les probabilités dénombrables et leurs applications arithmétiques. Rendiconti del Circolo Matematico di Palermo (1884-1940) 27(1), 247–271 (Dec 1909). https://doi.org/10.1007/BF03019651, https://doi.org/10.1007/BF03019651 [9] Cantelli, F.: Sulla probabilista come limita della frequencza. Rend. Accad. Lincei 26, 39 (1917) [10] Chatterjee, K., De Alfaro, L., Henzinger, T.A.: Trading memory for randomness. In: First International Conference on the Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings. p. 206–217. IEEE (2004) [11] Chatterjee, K., Piterman, N.: Combinations of qualitative winning for stochastic parity games. arXiv preprint arXiv:1804.03453 (2018) [12] De Alfaro, L.: Formal verification of probabilistic systems. stanford university (1998) [13] De Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332). p. 141–154. IEEE (2000) [14] Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05). p. 321–330. IEEE (2005) [15] Guenov, M., Barker, S.: Application of axiomatic design and design structure matrix to the decomposition of engineering systems. Systems Engineering 8, 29 – 40 (01 2005) [16] Guruji, A.K., Agarwal, H., Parsediya, D.: Time-efficient A* algorithm for robot path planning. Procedia Technology 23, 144–149 (2016) [17] Harel, D., Marron, A., Weiss, G.: Behavioral programming. Commun. ACM 55(7), 90–100 (2012) [18] Hart, S., Mas-Colell, A.: Uncoupled dynamics do not lead to nash equilibrium. American Economic Review 93(5), 1830–1836 (2003) [19] Kagan, E., Ben-Gal, I.: A group testing algorithm with online informational learning. IIE Transactions 46(2), 164–184 (2014) [20] Klein, D., Manning, C.D.: A* parsing: Fast exact viterbi parse selection. In: Proceedings of the 2003 Human Language Technology Conference of the North American Chapter of the Association for Computational Linguistics. p. 119–126 (2003) [21] Kupermann, O., Varfi, M.: Synthesizing distributed systems. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. p. 389–398. IEEE (2001) [22] Lazarus, A.J., Loeb, D.E., Propp, J.G., Stromquist, W.R., Ullman, D.H.: Combinatorial games under auction play. Games and Economic Behavior 27(2), 229–264 (1999) [23] Lewis, D.: Convention: A philosophical study. John Wiley & Sons (2008) [24] Pneuli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science. p. 746–757. IEEE (1990) [25] Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: Proceedings of the fifteenth annual ACM symposium on Theory of computing. p. 278–290 (1983) [26] Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and computation 103(1), 1–29 (1993) [27] Roijers, D.M., Vamplew, P., Whiteson, S., Dazeley, R.: A survey of multi-objective sequential decision-making. Journal of Artificial Intelligence Research 48, 67–113 (2013) [28] Schäfer, L., Christianos, F., Hanna, J.P., Albrecht, S.V.: Decoupled reinforcement learning to stabilise intrinsically-motivated exploration. In: Proc. 21st AAMAS. p. 1146–1154. IFAAMAS (2022) [29] Shiryaev, A., Chibisov, D.: Probability-1. Graduate Texts in Mathematics, Springer New York (2016) Appendix 0.A Appendix for Section 3 We first state well-known results from measure theory that we use in our proofs. Theorem 0.A.1(Carathéodory Extension Theorem [7]) Let Ω be a set and ℱ0F_0 be a field of subsets of Ω . Let P be a probability measure on ℱ0F_0. There exists a unique probability measure Q on σ(ℱ0)σ(F_0) such that Q(A)=P(A)Q(A)=P(A) for all A∈ℱ0A _0. Lemma 2(Borel-Cantelli lemmas [8, 9, 29]) Let E1,E2…,E_1,E_2…, be an infinite sequence of events in some probability space. First lemma: If ∑n=1∞Pr[En]<∞ _n=1^∞Pr[E_n]<∞, then the probability that infinitely many events occur is 0, namely Pr[lim supn→∞En]=0Pr[ _n→∞E_n]=0. Second lemma: If the events are all independent and ∑n=1∞Pr[En]=∞ _n=1^∞Pr[E_n]=∞, then almost-surely infinitely many of them occur, namely Pr[lim supn→∞En]=1Pr[ _n→∞E_n]=1. The Borel-Cantelli lemmas can be intuitively explained using a coin toss example. Suppose we are tossing a coin whose bias is varying over time. Let pip_i be the probability of seeing heads in the i-th toss. We are interested to know: if we toss the coin infinitely many times, will we see infinitely many heads? The first lemma says that if the infinite sum ∑i=1∞pi _i=1^∞p_i converges to a finite number, then the probability of seeing infinitely many heads is zero; an example would be pi=2−ip_i=2^-i. The second lemma says that if the infinite sum ∑i=1∞pi _i=1^∞p_i diverges to infinity, then the probability of seeing infinitely many heads is one; an example of this case would be pip_i being a constant. 0.A.1 Proof of Thm. 4 * Proof For the contrary, we suppose σ is a universal deterministic scheduler. In the following, we exhaustively explore all the possibilities of how σ may behave. Accordingly, we provide a game graph G, and for N=2N=2, a pair of objectives and policies which will violate the universality condition of σ. We consider the graph G as shown in Fig 2, where the set of vertices are V=v,a1,a2V=\v,a_1,a_2\, and the set of edges are E=(v,a1),(v,a2),(a1,v),(a2,v),(v,v)E=\(v,a_1),(v,a_2),(a_1,v),(a_2,v),(v,v)\. The initial vertex is v. Moreover, module 1 and 2’s target set of vertices is the singleton set consisting of a1a_1 and a2a_2, respectively. We describe the two exhaustive cases in the following: We construct two policies for which σ fails to maintain the universality condition. Let the infinite sequence p1p2⋯∈1,2ωp_1p_2…∈\1,2\^ω be the unique path produced by the deterministic scheduler σ. The only outgoing edge from vertex a1a_1 as well as from a2a_2 is the central vertex v. We define policy π1 _1 which behaves in the following manner: at the jthj th iteration, that is, after j time-steps have elapsed (assuming the game is at vertex v), if pj=1p_j=1, then π1 _1 prescribes taking the self-loop at v, and if pj=2p_j=2, then π1 _1 prescribes the edge (v,a1)(v,a_1). Similarly, we define π2 _2 as above replacing the role of 11 and 22. This makes the game stay at vertex v forever for the given scheduler σ. Thus, the implementation (,π1,π2,σ)⊧̸φ1∩φ2(G, _1, _2,σ) _1∩ _2, even though φ1∩φ2≠∅ _1∩ _2≠ and πi⊧φi _i _i for i=1,2i=1,2. ∎ 0.A.2 Proof of Thm. 5 * Proof Consider a fixed scheduler σ. We consider the following graph G in Fig.˜5, which consists of vertices V=v0,a1,a2,b1,b2V=\\,v_0,\;a_1,\;a_2,\;b_1,\;b_2\,\, and edges E=(v,ai),(a1,a1),(a1,v0),(a1,b1),(bi,v)∣i∈1,2E=\\,(v,a_i),\;(a_1,a_1),(a_1,v_0),(a_1,b_1),\;(b_i,v) i∈\1,2\\,\. We consider v0v_0 to be the initial vertex. We define the specifications φ1 _1 and φ2 _2 for modules 11 and 22 respectively by their Büchi sets that need to be visited infinitely often, where φ1 _1 requires that the vertex b1b_1 is seen infinitely often, and φ2 _2 requires that b2b_2 is seen infinitely often. The policies that we consider in the proof have the following shape. For module i∈1,2i∈\1,2\ that, when vertex v is visited for the nthn th time after which policy i is selected, the policy πi _i choses to go to vertex aia_i, and the policy πi _i then counts till a large value L(n)L(n) many steps and stays at vertex aia_i using the self-loop for L(n)L(n) many steps. After this L(n)L(n) many steps, then it proposes to visit vertex bib_i. This L(n)L(n) is an fast-increasing sequence constructed based on the scheduler σ. Since we have a fixed scheduler σ, we define the following events Lock1Lock_1 and Lock2Lock_2 Lockj=s∈1,2ω∣∃t∀r≥t:sr=jLock_j\;=\;\\,s∈\1,2\^ω ∃ t\ ∀ r≥ t:\ s_r=j\,\ Since σ induces a probability distribution PrσPr^σ on 1,2\1,2\, the values Prσ(Lockj)Pr^σ(Lock_j) is well-defined for j∈1,2j∈\1,2\. We call each visit to v an “attempt”, since process i, attempts to visits its Büchi state. For each “attempt” n≥1n≥ 1 and module j∈1,…,Nj∈\1,…,N\ define pn,j(L)=Prσ(indices at the n-th attempt start forming a block of L consecutive j’s),p_n,j(L)=Pr_σ (indices at the $n$-th attempt start forming a block of $L$ consecutive $j$'s ), pn,j(∞)=limL→∞pn,j(L)=Prσ(all indices from the n-th attempt start onward are j).p_n,j(∞)= _L→∞p_n,j(L)=Pr_σ (all indices from the $n$-th attempt start onward are j ). For a given scheduler σ one of the following is true: either (a) there exists a module j such that Prσ(Lockj)>0Pr_σ(Lock_j)>0; or (b) Prσ(Lock1)=Prσ(Lock2)=0Pr_σ(Lock_1)=Pr_σ(Lock_2)=0. (a) One module is chosen forever after a point with positive probability . There exists j with Prσ(Lockj)>0Pr_σ(Lock_j)>0. In this case, we can argue that the Büchi condition of the module that is not j is therefore cannot be achieved with at least this positive probability. (b) No module is chosen forever after a point with positive probability, the probability of seeing either module “forever” is 0. In this case, for both modules, that is modules j∈1,2j∈\1,2\, we have Prσ(Lockj)=0Pr_σ(Lock_j)=0; moreover, for each fixed time t∈ℕt and module j∈1,2j∈\1,2\, there are functions L1,L2:ℕ→ℕL_1,L_2\,:\,N such that limLj→∞Prσ(st=st+1=⋯=st+Lj−1=j)=0. _L_j→∞Pr_σ(s_t=s_t+1=·s=s_t+L_j-1=j)=0. Therefore, we show in the claim, that one can choose an increasing sequence Lj(n)→∞L_j(n)→∞ such that, for every finite collection of absolute starting times (tn)(t_n) corresponding to the intended attempt-starts, the probabilities of an Lj(n)L_j(n)-long block of j beginning at tnt_n are such that their summation is finite. vva1a_1a2a_2b1b_1b2b_2 Figure 5: This figure is redrawn for convenience. Red is module 1’s Büchi state, and Blue is module 2’s Büchi state Using our claim, and setting L(n)=maxL1(n),L2(n)L(n)= \L_1(n),L_2(n)\, we can construct policies having the shape discussed in the beginning of the proof. Recall the strategy is that when v is visited for the nthn th time stays at aia_i for L(n)L(n) many steps. Then it visits bib_i and returns. But the process j≠ij≠ i always wants to leave vertex aia_i back to v. The probability of visiting both b1b_1 and b2b_2 infinitely often then is 0, due to Borel-Cantelli lemma (Lemma˜2). Claim Assume that for all j∈1,2j∈\1,2\, Pr(Lockj=0)Pr(Lock_j=0). Then for each module j, there is an increasing sequence L(n)→∞L(n)→∞ (for a fixed scheduler σ) such that, for every finite collection of (tn)(t_n) corresponding to the intended attempt-starts, the probabilities of an L(n)L(n)-long block of scheduling the module j beginning at time tnt_n are such that their summation is finite. By our assumption this limit is 0 for every fixed t. Thus for each fixed t we have limL→∞pt,j(L)=0 _L→∞p_t,j(L)=0. We now construct L(n)L(n) inductively so that limn→∞L(n)=∞ _n→∞L(n)=∞ and ptn,j(L(n))p_t_n,j(L(n)) is small enough that the infinite sum is finite. Set L(0)=0L(0)=0. For n≥1n≥ 1 choose L(n)>L(n−1)L(n)>L(n-1) large enough that ptn,j(L(n))≤2−n−1.p_t_n,j (L(n) )≤ 2^-n-1. This is possible because ptn,j(L)→0p_t_n,j(L)→ 0 as L→∞L→∞. The sequence L(n)L(n) so obtained tends to infinity and satisfies ∑n=1∞ptn,j(L(n))≤∑n=1∞2−n−1=1/2, _n=1^∞p_t_n,j (L(n) )≤ _n=1^∞2^-n-1=1/2, as required. ∎ Appendix 0.B Appendix for Section˜4 Let WiW_i be the maximal set of vertices in G from which the agent i has a policy to fulfil φi _i. In other words, φi=(Wi) safe_i=Safe(W_i). Define W≔∩i∈[N]WiW _i∈[N]W_i. By assumption, W is nonempty, since v∈Wiv_ init∈ W_i for all i. Let [W]G[W] be the subgraph obtained by removing all the vertices V∖WV W from G, and by removing all the edges that involve these vertices. Proposition 1 The subgraph [W]G[W] is deadlock-free, meaning every vertex in W has a successor in W. Proof This follows from the mutual safety-closure: imagine, towards contradiction, that there is a vertex v∈Wv∈ W that has no successors. It follows that for every successor y of v in G, there exists a i∈[N]i∈[N] such that y∉Wiy∉ W_i. But this contradicts the mutual safety closure assumption, because every path $in$G ending at y is in ∩i∈[N]Wi=∩i∈[N](φi) _i∈[N]W_i= _i∈[N]Pref( _i), but not in (∩i∈[N]φi)Pref ( _i∈[N] _i ). We conclude that the subgraph [W]G[W] is deadlock-free. * Proof First observe that ∩i=1Nφi≠∅ _i=1^N live_i≠ , which follows from the assumption that ∩i=1nφi=∅ _i=1^n _i= , and that φi=φi∩φi _i= safe_i∩ live_i for every i. For each i∈[N]i∈[N], we write φi[W] live_i[W] to be the mapping of φi live_i as an objective in [W]G[W], defined as: φi[W]≔φi∩ℎ([W]) live_i[W] live_i _ inf(G[W]). We argue that φ1[W]∩…∩φN[W]≠∅ live_1[W]∩…∩ live_N[W]≠ . This follows from the assumption that φ1∩…∩φN≠∅ _1∩…∩ _N≠ in G, which implies that there is an infinite path $in$G that is in φi safe_i and φi live_i for every i∈[N]i∈[N]; in other words, ∩i∈[N]φi $isin$ _i∈[N] safe_i as well as in ∩i∈[N]φi _i∈[N] live_i. We first argue that Wω $mustbein$W^ω. If this were not the case, then there would be a largest prefix of W∗ $in$W^* (it exists, because v∈Wv_ init∈ W), before W $exits$W. However, since W=∩i∈[N]WiW= _i∈[N]W_i, and since, by Prop. 1, no path in [W]G[W] ends in a dead end, this would imply that Wi $wouldexitalsofromoneofthe$W_i-s, which would violate φi safe_i. Therefore, Wˆω$.Nowsince$∩_i∈[N]φ_i$,ittriviallyfollowsthat$Wˆω∩[∩_i∈[N]φ_i]∩[∩_i∈[N]φ_i]=∩_i∈[N]φ_i[W]$.Nowweshowthat$ℐ′=(,π_1,…,π_N,σ)ˆ⊧..(W)$.Suppose,forcontradiction′ssake,$Prˆℐ′((W))<1$.Thisimpliesthatthereisapath$∈ℎ∩Wˆ∗$in$$suchthat$Prˆℐ′()>0$,andthereexistsanagent$i$whoselects$v′$asasuccessorof$v$withpositiveprobabilitysuchthat$v′∉W$.Thismeans,thereexistsa$j∈[N]$suchthat$v′∉W_j$.However,byconstructionofshieldedimplementations,thisisnotpossible,sincethe$j$−thagentwould‘block′$v′$byexcludingitfromthesafesuccessorssenttoagent$i$,andagent$i$mustnotchoose$v′$inthiscase:acontradiction.Theaboveresultallowsustoignoretheverticesoutsideof$W$andfocuson$[W]$.Clearly,ifthepolicy$π_i$forevery$i$fulfills$φ_i$whileremaininginside$W$,bydefinition,itfulfills$φ_i[W]$,andviceversa.Moreover,fulfilling$(W)$automaticallyfulfills$∩_i=1ˆNφ_i$.Therefore,theclaimfollows.%usethedecoupledpoliciesobtainedfrom$[W]$(alongwiththemaximallypermissivesafetypolicies)asstatedabove.%Finally,byconstruction,$φ_1[W],…,φ_N[W]$arelivenessobjectivesin$[W]$,becausefromall$v∈W$,allobjectivesaresatisfiable.%Therefore,wecanusetherestrictionsfromthesafetyobjectivestosolvethedecoupledplanningproblemin$[W]$.∎ ∈ ^ω$.Nowsince$ $isalsoin$∩\_i∈[N] live\_i$,ittriviallyfollowsthat$ ∈ ^ω∩ [∩\_i∈[N] live\_i ]∩ [∩\_i∈[N] safe\_i ]=∩\_i∈[N] live\_i[W]$. Nowweshowthat$I =(G,π\_1,…,π\_N,σ) shld _ a.s.\!Safe(W)$.Suppose,forcontradiction ssake,$Pr^I (Safe(W))<1$.Thisimpliesthatthereisapath$ _ fin∩ W^*$in$G$suchthat$Pr^I ( )>0$,andthereexistsanagent$i$whoselects$v $asasuccessorof$v$withpositiveprobabilitysuchthat$v ∉ W$.Thismeans,thereexistsa$j∈[N]$suchthat$v ∉ W\_j$.However,byconstructionofshieldedimplementations,thisisnotpossible,sincethe$j$-thagentwould``block $v $byexcludingitfromthesafesuccessorssenttoagent$i$,andagent$i$mustnotchoose$v $inthiscase:acontradiction. Theaboveresultallowsustoignoretheverticesoutsideof$W$andfocuson$G[W]$.Clearly,ifthepolicy$π\_i$forevery$i$fulfills$ live\_i$whileremaininginside$W$,bydefinition,itfulfills$ live\_i[W]$,andviceversa.Moreover,fulfilling$Safe(W)$automaticallyfulfills$∩\_i=1^N safe\_i$.Therefore,theclaimfollows.%usethedecoupledpoliciesobtainedfrom$G[W]$(alongwiththemaximallypermissivesafetypolicies)asstatedabove.%Finally,byconstruction,$ live\_1[W],…, live\_N[W]$arelivenessobjectivesin$G[W]$,becausefromall$v∈ W$,allobjectivesaresatisfiable.%Therefore,wecanusetherestrictionsfromthesafetyobjectivestosolvethedecoupledplanningproblemin$G[W]$. proof Appendix 0.C Appendix for Section˜6 * Proof Let =(V,E,v0)G=(V,E,v_0), σ, and π1,…,πN _1,…, _N be N path-aware policies. We prove that for each module i∈[N]i∈[N], under the induced measure PrℐPr^I on ℎ()Paths_ inf(G), the event that the objective φi _i is satisfied has probability 11. Since a finite intersection of almost-sure events has probability 11, this establishes the theorem. For every history u∈[N]⋆u∈[N] and each index j∈[N]j∈[N], we have σ(u)(j)≥ϵ>0σ(u)(j)≥ε>0. Fix any module i and let LiL_i be the uniform bound on its hitting time. Consider the sequence of scheduler choices P0,P1,…P_0,P_1,… defined by the random variables Pk:[N]ω→[N]P_k:[N]^ω→[N] selecting the scheduler’s output at time k. For each n≥0n≥ 0, define the event Eni=Pn=Pn+1=⋯=Pn+Li−1=i,E_n^i\;=\;\\,P_n=P_n+1=·s=P_n+L_i-1=i\,\, that is, the scheduler chooses module i for LiL_i consecutive steps starting at position n. For every history u∈[N]nu∈[N]^n, Pr(Eni|P0…Pn−1=u)≥ϵLi.Pr (E_n^i\, |\,P_0… P_n-1=u )\;≥\;ε^L_i. Therefore, each event EniE_n^i has strictly positive conditional probability, uniformly bounded below by ϵLiε^L_i. Claim With probability 11, infinitely many of the events EniE_n^i occur. Proof of claim: Due to the events not being independent, instead of using Borel-Cantelli’s second lemma directly, we instead define the stopping times T0i=0T_0^i=0 and inductively Tk+1i=minn>Tki∣Eni occursT_k+1^i= \\,n>T_k^i E_n^i occurs\,\. Because ϵLi>0ε^L_i>0, the conditional probability that no EniE_n^i ever occurs after time TkiT_k^i is zero. This implies that the event “only finitely many EniE_n^i occur” has measure 0. Equivalently, Prℐ(Eni infinitely often)=1.Pr^I(E_n^i infinitely often)=1. Hence, almost surely, the scheduler produces infinitely many disjoint blocks of length LiL_i in which module i is scheduled exclusively. ■ Claim Conditioned on EniE^i_n occuring infinitely often, the Büchi condition is satisfied almost-surely. Proof of claim: Fix such a block of length LiL_i in which only module i is active. Assuming uniform bounded hitting time, starting from any vertex v and any policy πi _i executed for LiL_i consecutive steps guarantees that the corresponding path visits the target set BiB_i with positive probability. Because there are infinitely many such exclusive activation blocks for module i, it follows that almost surely the infinite path generated by the implementation visits BiB_i infinitely often. ■ For reachability objectives, the same argument applies (with “at least once” instead of “infinitely often”). Finally, since φ1,…,φN _1,…, _N are finitely many, Prℐ(⋂i=1Nφi)=1−Prℐ(⋃i=1Nφi¯)=1,Pr^I ( _i=1^N _i )=1-Pr^I ( _i=1^N _i )=1, and hence the implementation (,π1,…,πN,σ)(G, _1,…, _N,σ) almost surely satisfies the conjunction of all objectives. Appendix 0.D Appendix for Section˜7 0.D.1 Proof of Thm. 7 * Proof We give an explicit graph G, specifications φ1 _1, and φ2 _2, and policies π1 _1 and π2 _2, independent of the scheduler σ, and then show the implementation fails to satisfy the intersection of the specifications. Let V=v0,v1,v11,v12,V=\v_0,\;v_1,\;v_11,\;v_12\, where the initial vertex is v0v_0, and the edges E=(v0,v0),(v0,v1),(v1,v11),(v1,v12),(v11,v0),(v12,v0)E\>=\>\\,(v_0,v_0),(v_0,v_1),(v_1,v_11),\ (v_1,v_12),(v_11,v_0),(v_12,v_0)\,\. We define coBüchi specifications by their coBüchi sets that need to be visited only finitely often where φj _j requires that the vertex v1jv_1j is seen only finitely often along the infinite path. Note that there are paths that avoid both v12v_12 and v21v_21 forever (e.g. a path that loops at v0v_0), so φ1∩φ2≠∅ _1∩ _2≠ . v0v_0v1v_1v11v_11v12v_12 Figure 6: Graph G used in the proof of Section˜7. Figure is redrawn from Fig.˜4. Red (v11v_11) is the coBüchi vertex for φ1 _1; blue (v12v_12) is the coBüchi vertex for φ2 _2; The strategy edge for module 11 is highlighted in red, and the strategy edge for module 2 is highlighted in blue. We define deterministic policies π1,π2:V⋆→V _1, _2:V → V below that satisfy φ1 _1 and φ2 _2 respectively. π1(v0)=v1,π1(v1)=v12,π1(v1j)=v0for j=1,2 array[]l _1(v_0)=v_1,& _1(v_1)=v_12,\\ _1(v_1j)=v_0\ for j=1,2 array π2(v0)=v1,π2(v1)=v11,π2(v1j)=v0for j=1,2 array[]l _2(v_0)=v_1,& _2(v_1)=v_11,\\ _2(v_1j)=v_0\ for j=1,2 array Consider a scheduler σ. Since the policies are such that they make the same decision at all vertices other than v1v_1, we focus on the scheduler σ’s decision at vertex v1v_1. We deal with two cases. Either one module is eventually always scheduled with non zero probability when the token is at vertex v1v_1, or with probability 11, both modules are scheduled infinitely often. Some module is eventually always scheduled at vertex v1v_1. for some j∈1,2j∈\1,2\, Prσ(eventually only j)=Prσ(∃T∀t≥T:indext=j)>0.Pr^σ(eventually only j)\>=\>Pr^σ (∃ T\ ∀ t≥ T:\ index_t=j )>0. On the event that the scheduler eventually plays only j, the implementation (,π1,π2,σ)(G, _1, _2,σ) follows the single policy πj _j from some time on. If j=1j=1 then from that time T onward the execution follows π1 _1 and therefore visits v12v_12 (the bad state for φ2 _2) infinitely often (indeed on each visit to v1v_1 it goes to v12v_12, so φ2 _2 is violated on this event. Hence the event “scheduler eventually plays only 1” implies violation of φ2 _2. The probability that both φ1 _1 and φ2 _2 hold is at most 1−Prσ(eventually only 1)<11-Pr_σ(eventually only 1)<1. The holds if the scheduler eventually selects only module 2. Thus in either case the intersection is not satisfied almost surely. No module is eventually always scheduled at vertex v1v_1. In this case, Prσ(∃T∀t≥T:indext=j)=0Pr_σ(∃ T\ ∀ t≥ T:\ index_t=j)=0 for j=1,2j=1,2. Then with probability one the scheduler produces infinitely many occurrences of both indices 11 and 22 (otherwise, if some index occurred only finitely often with positive probability that would give a positive-probability lock event). Consequently, along almost all scheduler index-sequences, both modules are scheduled infinitely often. Under such a scheduler sample path, both indices occur infinitely often, the execution will visit v11v_11 infinitely often and v12v_12 infinitely often (in fact infinitely many alternating occurrences typically), so both coBüchi conditions are violated. Therefore in this case the implementation does not satisfy φ1∩φ2 _1∩ _2 with probability 11. 0.D.2 Proof of Thm. 7.1 * Proof We describe the global interaction between N agents as an absorbing Markov chain ℒL. Note that all policies have the same set of memory states M=ℎ()×ℭBM=Paths_ fin(G)× C_B. A state of the Markov chain is ⟨m1,…,mN⟩,v⟩∈MN×V m_1,…,m_N ,v ∈ M^N× V. A state is called consensus if mj=mj′m_j=m_j , for all j,j′∈1,…,Nj,j ∈ \1,…,N \, dually every other state is reffered to as non-consensus. A consensus state ⟨m,…,m⟩,v⟩ m,…,m ,v is called a sink if m=⟨ϵ,C⟩m= ε,C for some cycle C, and the current vertex is already inside C. Note that such a sink state corresponds to the case that all policies chooses the same cycle C, thus the path that they generate will be CωC^ω, which satisfies all objectives since C∈ℭBjC∈ C_B_j for all j∈1,2,…,Nj∈ \1,2,…,N \. Note that such a global state corresponds to the case that all policies choose the same path η and cycle C, thus the path that they generate will be η⋅Cωη· C^ω, which satisfies all objectives since C∈ℭBjC∈ C_B_j, for all j∈1,…,Nj∈ \1,…,N \. The probability of transitioning from ⟨m1,…,mN⟩,v⟩ m_1,…,m_N ,v to ⟨m1′,…,mN′⟩,v′⟩ m _1,…,m _N ,v is ∑j=1Nσ(j)⋅πj(v,mj,⊤)(mj′,v′)⋅∏j′≠jπj′(v,mj′,⊥)(mj′,v′) _j=1^Nσ(j)· _j(v,m_j, )(m _j,v )· _j ≠ j _j (v,m_j , )(m _j ,v ) Claim ℒL is indeed a finite Markov chain Proof of claim: We show that the sum over all the outgoing non-zero transition probabilities is indeed 11 for any state l of ℒL. Fix l=⟨m1,…,mN⟩,v⟩l= m_1,…,m_N ,v . Let the next state be l′=⟨m1′,…,mN′⟩,v′⟩l = m _1,…,m _N ,v . Then: ∑l′P(l,l′) _l P(l,l ) =∑m→′∈MN,v′∈V∑j=1Nσ(j)⋅πj(v,mj,⊤)(mj′,v′)⋅∏k≠jπk(v,mk,⊥)(mk′,v′) = _ m ∈ M^N,v ∈ V _j=1^Nσ(j)· _j(v,m_j, )(m _j,v )· _k≠ j _k(v,m_k, )(m _k,v ) =∑j=1Nσ(j)∑v′∈V(∑mj′∈Mπj(v,mj,⊤)(mj′,v′)⋅∏k≠j[∑mk′∈Mπk(v,mk,⊥)(mk′,v′)]) = _j=1^Nσ(j) _v ∈ V ( _m _j∈ M _j(v,m_j, )(m _j,v )· _k≠ j [ _m _k∈ M _k(v,m_k, )(m _k,v ) ] ) Note that for k≠jk≠ j, the sum over their local next messages mk′m _k equals 11 regardless of v′v . Thus the product term simplifies to 11: =∑j=1Nσ(j)∑v′∈V∑mj′∈Mπj(v,mj,⊤)(mj′,v′) = _j=1^Nσ(j) _v ∈ V _m _j∈ M _j(v,m_j, )(m _j,v ) Similarly, the inner sum over the active agent’s transition leads to 1: =∑j=1Nσ(j)⋅1 = _j=1^Nσ(j)· 1 =1. =1. ■ We also make the claim below. Claim Every bottom strongly connected components (BSCC) of the Markov chain only consists of sink states, and each sink state is part of some (plausibly singleton) BSCCs. Since a finite Markov chain eventually reaches a BSCC with probability 11, it suffices to conclude that (,π1,…,πN,σ)⊧..⋀1≤i≤Nφi(G, _1,…, _N,σ) _ a.s.\! _1≤ i≤ N _i. ∎ Proof of claim: We establish the above claim by showing the following three properties of the constructed Markov chain: (1) the probability of transitioning from any consensus state to a non-consensus one is 0 (as a corollary, it holds for the special case of a sink to a non-sink state), (2) from any non-consensus state, there exists a path with probability >0>0 to some consensus state, and finally, (3) the probability of transitioning from any non-sink consensus state ⟨m=⟨η,C⟩,…,m⟩,v⟩ m= η,C ,…,m ,v to another non-sink consensus state ⟨m′=⟨η′,C⟩,…,m′⟩,v′⟩ m = η ,C ,…,m ,v is >0>0, only if η′=η[1:]η =η[1:]. (1) implies that a consensus and a non-consensus state cannot be part of same SCC. (2) (together with (1)) establishes that non-consensus states cannot be a part of any BSCC. Finally, (3) shows that two non-sink consensus states cannot be in the same SCC. To show (1), we consider an arbitrary consensus state ⟨m,…,m⟩,v⟩ m,…,m ,v , and an arbitrary non-consensus state ⟨m1′,…,mN′⟩,v′⟩ m_1 ,…,m_N ,v where mj′≠mj′m_j ≠ m_j for some j,j′∈[N]j,j ∈[N]. We argue that each summand in the expression of the transition probability is 0. Fix an arbitrary j∈[N]j∈[N]. If πj(v,m,⊤)(mj′,v′)=0 _j(v,m, )(m_j ,v )=0, we are done. Otherwise, we have πj(v,m,⊤)=(mj′,v′) _j(v,m, )=(m_j ,v ) (since πj _j is deterministic), and at least one j′∈[N]j ∈[N] such that mj′≠mj′m_j ≠ m_j . We consider πj′(v,m,⊥)(v′,mj′) _j (v,m, )(v ,m_j ), and show that this is 0. Since both πj _j and πj′ _j are defined using the same π constructed above, πj′(v,m,⊤)=πj(v,m,⊤) _j (v,m, )= _j(v,m, ), we have πj′(v,m,⊤)=(mj′,v′) _j (v,m, )=(m_j ,v ). Therefore, from mj≠mj′m_j≠ m_j , we have πj′(v,m,⊥)(mj′,v′)=0 _j (v,m, )(m_j ,v )=0. To show (2), we consider an arbitrary non-consensus state ⟨m1,…,mN⟩,v⟩ m_1,…,m_N ,v , and construct a path with positive probability to a consensus state in the following manner: we first divide the policies 1,2,…N1,2,… N in at most degree(v)degree(v)-many (plausibly empty) sets, namely X1,…,Xdegree(v)X_1,…,X_degree(v), where each set XiX_i correspond to a neighbouring vertex u of v such that all the policies in XiX_i proposes u as its next action. We first assume that at least two of these sets are non-empty, and select a set, namely XlX_l, with the least number of policies. We then select a policy from XlX_l, namely policy j. Suppose πj(v,mj,⊤)=(v′,m′) _j(v,m_j, )=(v ,m ). We know σ(j)>0σ(j)>0. Moreover, for any policy j′∈∪i≠lXij ∈ _i≠ lX_i , πj′(v,mj′,⊥)(v′,m′)>0 _j (v,m_j , )(v ,m )>0. Therefore, there exists an edge with positive probability from ⟨m1,…,mN⟩,v⟩ m_1,…,m_N ,v to ⟨m1′,…,mN′⟩,v′⟩ m_1 ,…,m_N ,v with mj′=m′m_j =m for all j′∈j∪⋃l≠iXlj ∈\j\∪ _l≠ iX_l. Since XlX_l is of size at most N2 N2, upon traversing along this edge consensus among at least N2+1 N2+1 many policies is achieved. If ⟨m1′,…mN′⟩,v′⟩ m_1 ,… m_N ,v is a consensus state, we are done; otherwise, we apply the same procedure from ⟨m1′,…,mN′⟩,v′⟩ m_1 ,…,m_N ,v , and so on untill it converges to a consensus state. Note that, in the second step, at least N2+1 N2+1 many policies will be in the same set, therefore the size of smallest set could be at most N2−1 N2-1. Therefore, the procedure reaches to a consensus state within at most N-steps, if in every step there are at least two non-empty sets. Finally, we argue that this assumption does not prevent reaching the consensus, albeit delay it. Suppose at some step, there is only a single non-empty set, it means that all the policies agree in their action in that step. If this happens at a non-consensus state, we know eventually their proposed action will differ, so till then we simply traverse along non-consensus states in the Markov Chain without improving the consensusness. Finally, showing (3) is straightforward: since, every policy has the same memory state at a given vertex v, no matter which policy is scheduled, each of them updates along the path to the cycle. Since by assumption, we consider only simple path to the cycle, there can be edge with probability >0>0 in only one of the direction. ■ Appendix 0.E Appendix for Section˜8 0.E.1 Proof of Lem. 1 Proof Consider an infinite path γ that is good for all pairty objective κi _i. Let ai∈inf(γ)a_i∈ (γ) for each i∈[N]i∈[N] be the states that maximises κi _i. Since γ satisfies each κi _i’s, κi(ai) _i(a_i) is even. Since each of aia_i is visited infinitely often in γ, without loss of generality, we assume that there is a path τi _i from aia_i to ai+1a_i+1 for i=[N−1]i=[N-1], and a path τN _N from aNa_N to a1a_1 such that each vertex inside τi _i is visted infinitely often in γ for every i∈[N]i∈[N]. Obtain τi′ _i from τi _i by deleting all the cycles. Observe the cycle τ1′⋅τ2′⋯τN′ _1 · _2 ·s _N . The maximal parity index in κi _i that the cycle traverses is κi(ai) _i(a_i) for each i. In other words, (τ1′⋅τ2′⋯τN′)ω( _1 · _2 ·s _N )^ω satisfies each parity objective κi _i. Fix an arbitray i∈[N]i∈[N], and we describe θi _i: for any vertex a∈τi′a∈ _i , and for its successor vertex a′∈τi′a ∈ _i , θi(a)=a′ _i(a)=a ; for any state a∈γ(i+1)modNa∈ _(i+1) N for which θi _i is yet to be defined, and its successor a′∈γi+1modNa ∈ _i+1 N, we define θi(a)=a′ _i(a)=a , and so on till we exhaust all the vertices of γi+(N−1)modN _i+(N-1) N. For any other vertex a∈Va∈ V, we define all θi _i to choose the same successor, one that leads closer to the cycle τ1′⋅τ2′⋯τN′ _1 · _2 ·s _N . Note that, each θi _i is memoryless. By asumption σ schedules every agent infinitely often at every vertex, thus we note that in any path δ with non-zero measure, inf(δ) (δ) is the set of vertices of the cycle τ1′⋯τN′ _1 ·s _N . Since, the cycle satisfies all the parity objectives κi _i, the implementation almost-surely satisfies κi _i for each i∈[N]i∈[N]. ∎ 0.E.2 Proof of Thm. 1 * Proof We describe the global interaction between N policies as an absorbing Markov chain. Note that all policies have the same set of memory states M=(V)NM=(V^V)^N. A state of the Markov chain is ⟨m1,m2,…mN⟩,v⟩∈(V)N×V m_1,m_2,… m_N ,v ∈(V^V)^N× V, where each mi=⟨θi,1,θi,2,…θi,N⟩m_i= _i,1, _i,2,… _i,N . Recall that, θi,j _i,j denotes the memoryless policy that Agent i thinks Agent j would play (for i=ji=j, it is the policy Agent i intends to play if scheduled). For each state l of ℒL, we define a set used-edges UlU_l as follows: an edge e=(u,w)e=(u,w) is in UlU_l if there is an agent i such that θi,i(u)=v _i,i(u)=v. A vertex u is called conflicting at a state l if there exists Agent i,ji,j such that θi,i(u)≠θi,j(u) _i,i(u)≠ _i,j(u). A state l is called consensus if in the graph G restricted to the set used-edges UlU_l of l, a conflicting vertex u of l is not reachable from v. Intuitively speaking, a state is called consensus if every agent correctly guesses about every other agents’s memoryless policies, possibly except for the vertices which are anyway not reachable from v. Every other states are referred to as non-consensus. Once it reaches a consensus state, none of the memory states ever change. Recall that implementation of a fair scheduler on each memory state mim_i, by design, almost surely satisfies κi _i. Therefore, when mi=m_i=m for some memory state m for all i∈[N]i∈[N], the implementation of σ on ⟨m,…,m⟩ m,…,m almost surely satisfies all the parity objectives. It remains to show that no matter from which state of the Markov chain the procedure starts, it always reaches a consensus state. We first define the transition probabilities from ⟨m1,…,mN⟩,v⟩ m_1,…,m_N ,v to ⟨m1′,…mN′⟩,v′⟩ m_1 ,… m_N ,v as follows: ∑j=1Nσ(j)⋅πj(v,mj,(j,v′))(mj′,v′)∏j′≠jπj′(v,mj′,(j,v′))(mj′,v′) _j=1^Nσ(j)· _j(v,m_j,(j,v ))(m_j ,v ) _j ≠ j _j (v,m_j ,(j,v ))(m_j ,v ) We first show that it is indeed a Markov Chain. Claim ℒL is a Markov chain. Proof of claim: We show that the sum over all the outgoing non-zero transition probabilities is indeed 11 for any state l of ℒL. Fix an l=⟨m1,…mN⟩,v⟩l= m_1,… m_N ,v . Then, ∑⟨m1′,…,mN′⟩,v′⟩∈MN×V _ m_1 ,…,m_N ,v ∈ M^N× V ∑j=1Nσ(j)⋅πj(v,mj,(j,v′))(mj′,v′)⋅∏j′≠jπj′(v,mj′,(j,v′))(mj′,v′) _j=1^Nσ(j)· _j(v,m_j,(j,v ))(m _j,v )· _j ≠ j _j (v,m_j ,(j,v ))(m _j ,v ) =∑j=1Nσ(j)∑MN×Vπj(v,mj,(j,v′))(mj,v′)⋅∏j′≠jπj′(v,mj′,(j,v′))(mj′,v′) = _j=1^Nσ(j) _M^N× V _j(v,m_j,(j,v ))(m_j,v )· _j ≠ j _j (v,m_j ,(j,v ))(m _j ,v ) =∑j=1Nσ(j)∑MN−1×V⋅∏j′≠jπj′(v,mj′,(j,v′))(mj′,v′) = _j=1^Nσ(j) _M^N-1× V· _j ≠ j _j (v,m_j ,(j,v ))(m _j ,v ) =∑j=1Nσ(j)∑MN−2×V∏j′≠j,j′πj′(v,mj′,(j,v′))(mj′,v′)∑Mπj′(v,mj′,(j,v′))(mj′,v′) = _j=1^Nσ(j) _M^N-2× V _j ≠\j,j \ _j (v,m_j ,(j,v ))(m_j ,v ) _M _j (v,m_j ,(j,v ))(m_j ,v ) =∑j=1Nσ(j)∑MN−2×V∏j′≠j,j′πj′(v,mj′,(j,v′))(mj′,v′) = _j=1^Nσ(j) _M^N-2× V _j ≠\j,j \ _j (v,m_j ,(j,v ))(m_j ,v ) ⋮ =∑j=1Nσ(j)=1 = _j=1^Nσ(j)=1 ■ Since a finite Markov chain eventually reaches a BSCC with probability 11, it suffices to show that consesus states are BSCCs of this Markov Chain. Formally, Claim Every BSCC of ℒL only consists of consensus states. Proof of claim: We establish the above statement by showing the following three properties: (1) The transition probability from any consensus state to any non-consensus state is 0, (2) For any non-consensus state, there exists a path with probability >0>0 to some consensus state, and finally, (3) there exists at least one consensus state in ℒL. Since, ℒL has no dead-end by design, this proves the claim. To show (1), we consider an arbitrary consensus state ⟨m,…,m⟩,v⟩ m,…,m ,v , and an arbitrary non-consensus state ⟨m1′,…,mN′⟩,v′⟩ m_1 ,…,m_N ,v where mj′≠mj′m_j ≠ m_j for some j,j′∈[N]j,j ∈[N]. We argue that each summand in the expression of the transition probability is 0. Fix an arbitrary j∈[N]j∈[N]. If πj(v,m,(j,v′))(mj′,v′)=0 _j(v,m,(j,v ))(m_j ,v )=0, we are done. Otherwise, we have πj(v,m,(j,v′))=(mj′,v′) _j(v,m,(j,v ))=(m_j ,v ) (since πj _j is deterministic in this case), and at least one j′∈[N]j ∈[N] such that mj′≠mj′m_j ≠ m_j (since we consider a non-consensus state). We consider πj′(v,m,(j,v′))(mj′,v′) _j (v,m,(j,v ))(m_j ,v ), and show that this is 0. Since both πj _j and πj′ _j are defined using the same π constructed above, πj′(v,m,(j,v′))=πj(v,m,(j,v′)) _j (v,m,(j,v ))= _j(v,m,(j,v )), we have πj′(v,m,(j,v′))=(mj′,v′) _j (v,m,(j,v ))=(m_j ,v ). Therefore, from mj≠mj′m_j≠ m_j , we have πj′(v,m,(j,v′))(v′,mj′)=0 _j (v,m,(j,v ))(v ,m_j )=0. To show (2), we consider an arbitrary non-consensus state l=⟨m1,…,mN⟩,v⟩l= m_1,…,m_N ,v , with mi=⟨θi,1,…θi,N⟩m_i= _i,1,… _i,N and construct a path with positive probability to a consensus state in the following. At any state s, for each agent i, we denote by Xi(s)X_i^(s) the set of agents i′i for which θi,i≠θi′,i _i,i≠ _i ,i, and by Yi(s)Y_i^(s) the set of agents i for which θi,i(u)≠θi′,i(u) _i,i(u)≠ _i ,i(u), where u is the location at s. Clearly, Yi(s)⊆Xi(s)Y_i^(s) X_i^(s) for any i and s. Since l is a non-consensus state, there exists at least one agent i for which Xi(l)X_i^(l) is non-empty. Otherwise, we are already at a consensus state! We know σ(i)>0σ(i)>0. Without loss of generality, we assume that Yi(l)Y_i^(l) is also non-empty. We consider the scenario when Agent i is scheduled, which makes the next vertex θi,i(v)=v′ _i,i(v)=v . Since every agent i′i of Yi(l)Y_i^(l) makes a wrong guess about Agent i, with positive probability, all of them changes their memory state to mim_i. In other words, there exists an edge from l to l′=⟨m1′,…,mN′⟩,v′⟩l = m_1 ,…,m_N ,v , where mi′=mim_i =m_i for all i′∈Yi(l)i ∈ Y_i^(l), making Xi(l′)=Xi(l)∖Yi(l)X_i^(l )=X_i^(l) Y_i^(l). If l′l is a consensus state, we are done. Otherwise, we select another agent j for which Xj(l′)X_j^(l ) is non-empty, and continue the procedure. Note that, once two agents reaches a consensus in their memory state, with positive probability, they never lose that consensus again. This is because from that point onwords, either both of them requires change of memory (when both of their guessed policy about some third agent turns out to be wrong) or none of them changes policy. So, when they require to change, they can change their memory states to yet another same memory state with positive probability. Therefore, in this path, for any state s, the size of at least one Xi(s)X_i^(s) is decreasing if there is at least one i with non-empty Yi(s)Y_i^(s). If Yi(s)Y_i^(s) is empty for all i at some non-consensus statess at some step, with positive probability, we add an edge to the path where the consensus remains the same. Since by definition of consensus state, a conflicting vertex u is always reachable, we follow that path from v by scheduling the agents appropriately. Yet again, we can do this with probability >0>0. In this manner, we have a path with positive probability from a non-consensus state l′l with no conflicting vertex to a non-consensus vertex l′l with conflicting vertices. From l′l , we follow the previously mentioned procedure to go to a state with improved consensus with positive probability. Iterating these two procedures, we get a path from non-consensus state to a consensus state with probability >0>0. Finally, property (3) is established in Lemma 1. ■