Towards a Unified View of Social Laws with Instantaneous Actions

1 Introduction

Autonomous agents and multi-agent systems have been extensively studied across different sub-fields of AI. A core challenge in complex, multi-agent environments is that in order for an agent to choose a course of action, it must account for both its own actions and those of the other agents. We consider a setting in which non-collaborative agents operate in a shared environment, particularly where self-interested agents risk unintentionally disrupting each other's activities. In such cases, a centralized planning algorithm that designs and coordinates individual plans is impractical.

The social law approach [Tenneholtz and Moses, 1989; Shoham and Tennenholtz, 1992] offers a means of imposing implicit coordination, and enables each agent to plan independently, while the system design aims to minimizes conflicts between the different plans. Social laws (SL) restrict permissible behaviors, akin to real-world traffic laws, where drivers follow rules to maintain collective safety. These laws, despite being restrictive, still permit every driver to reach their designated locations, i.e., these laws are robust. Generally, a SL is robust if it prevents conflicts among agents, ensuring each can reach its goal.

While the concept of SLs is general, it does not always specify how each agent chooses its actions. We are concerned with planning-based SLs - that is, applying SL to systems in which agents must choose a long-term course of action - agents must plan. Previous work on planning-based SLs [Karpas et al., 2017] demonstrated that verifying the robustness of a SL in multi-agent (classical) planning can be reduced to a classical planning problem - the robustness verification problem. The objective of the robustness verification problem is to find a counterexample: if the compiled problem is unsolvable, then the SL is robust. Later work [Nir et al., 2023] extended this approach to numeric planning, introducing a modified compilation to numeric planning that accounts for violations of numeric action preconditions.

In this paper, we propose a new compilation for verifying the robustness of a SL in a multi-agent planning system. Our approach is more general than previous methods, as it treats interference details between actions as independent of the compilation, determined by an external procedure. Thus, our new compilation can handle both numeric and classical planning formalisms, as well as any new formalism - provided (a) actions are instantaneous, and (b) we can efficiently compute the negation of the preconditions of every action. Note that our compilation uses the same features as the multiagent (input) problem. That is, if the multi-agent problem has numeric variables, the compiled problem will have numeric variables as well. However, if the original problem only has classical preconditions/effects, the compiled problem will be classical.

A more general compilation might lead to a performance drop; however, our empirical evaluation demonstrates that solving the robustness verification problem from our new compilation is comparable to that of previous methods, maintaining state-of-the-art performance. Moreover, treating action preconditions as general logical formulas is a first step towards the integration of planning-based SLs with research on social norms [ ˚Agotnes et al., 2010; ˚Agotnes andWooldridge, 2010; ˚Agotnes et al., 2012], which explores a modal logic of norm compliance.

(c) Plan 2

Figure 1: Illustrative Example

2 Preliminaries

Deterministic Multi-Agent Problem Formalism In this work we deal with problems represented in a formalism inspired by the work of Brafman and Domshlak ¨ıs more general, than previous methodsbrafman-domshlak:icaps-2008, in which each agent has its own goal [Karpas et al., 2017]. Such a problem is given by Π = ⟨V, {Ai}ni=1 , I, {Gi}ni=1 ⟩, where V is the set of variables (boolean, finite-domain or numeric), {Ai} is the set of actions available to agent i (each agent is numbered from [n] := {1, . . . , n}). The set of states S is a full assignment on the variables in V. A computable boolean formula f over the variables in V is called a condition, and it can be either true or false. We say that a state s ∈ S satisfies the conditions f, s |= f, if the formula f is true under the assignment of the values of s to f. For a set of conditions F, we say that s |= F if s |= f for each f ∈ F. Each action is a tuple ⟨pre(a), eff(a)⟩, where pre(a) is a set of computable boolean formulas over V, and eff(a) is a set of changes (modeled as assignments to state variables) the action a applies to the values of s. We say that a is applicable in s if s |= pre(a). We also assume that the changes introduced by a to s are well-defined, i.e., eff(a) affects each variable at most once and the resulting value lies within the domain of the variable, while variables that are not affected by eff(a) keep their values. We assume that both preconditions and effects are computable in polynomial time. The result of applying an (applicable) action a to the state s is denoted by s�a�. The initial state I is a state. Agent i ∈ [n] has its own goal Gi, a set of conditions on V.

For a single agent i, a planning task is given as a tuple Πi := ⟨V,Ai, I,Gi⟩. In the literature these are often called simply planning tasks. In what follows such tasks are represented with a single set of actions and goals. The result of sequentially applying (if possible) the sequence of actions π to the state s is denoted by s�π�. The sequence of actions πi = ⟨a1, . . . , am⟩ is called an individual plan if I�πi� |= Gi and aj ∈ Ai for each j ∈ [m]. πi is also a plan for the planning task ⟨V,Ai, I,Gi⟩. A joint plan is a consecutively applicable sequence of actions π such that I�π� |= ⋃ni=1 Gi. Consequently, π is a plan for the task Πc := ⟨V, ⋃ni=1 Ai, I, ⋃ni=1 Gi⟩.

Running Example Consider an example with 2 agents (solid red and dashed blue, denoted R and B, respectively) in a 2x3 grid (cells are denoted NW, NE, CW, CE, SW, SE for north-west, north-east, central-west, central-east, south-west, south-east, respectively). Initially R is at NE and B is at SW.

Their goals are to reach CW and CE, respectively. This is depicted in Figure 1a, where initial positions are depicted with IR, IB and goals with GR, GB.

We encode this problem in our formalism using 2 finite domain variables: V = {loc(R), loc(B)}, which denote the locations of each agent. Both variables share a domain, dom(loc(B)) = dom(loc(R)) = {NW,NE, CW, CE, SW, SE}. In the initial state I we have loc(B) = SW and loc(R) = NE, while the goals are GB = {loc(B) == CE} and GR = {loc(R) == CW}.

Each agent has 14 move actions corresponding to possible moves from each of the 6 different locations - 2 from each corner, 3 from the center positions. The action for moving agent i from location l1 to adjacent location l2 is denoted move(i, l1, l2) where i ∈ {R,B}, l1 ∈ {NW,NE, CW, CE, SW, SE}, and l2 iterates over the adjacent locations to l1 (for example, if l1 = NW, l2 iterates over NE and SW). The action preconditions check that agent i is indeed at location l1, and that the other agent (denoted -i) is not at l2, so as not to crash into it. This is given by pre(move(i, l1, l2)) = {loc(i) == l1, loc(-i) ̸= l2}. The effects of move(i, l1, l2)) change the location of agent i to l2, that is, eff(move(i, l1, l2)) = {loc(i) ← l2}. Thus, the actions of agent i are Ai = {move(i, l1, l2) | l1 ∈ {NW, NE, CW, CE, SW, SE}, l2 adjacent to l1}.

Social Laws Inmulti-agent systems, a common issue arises when agents' individual plans conflict. For instance, two agents may need the same unique tool for their tasks. If the first agent uses the tool and fails to return it to the toolbox, this prevents the second agent from completing its task.

Returning to our running example, the two individual plans depicted in Figure 1b (consisting of πB = ⟨move(B, SW, CW),move(B, CW, CE)⟩ and πR = ⟨move(R,NE, CE),move(R, CE, CW)⟩) conflict, as the two agents might collide, that is, one of the preconditions of one of the actions will be violated. The exact action that will fail depends on the timing - when each action is executed. For example, if the joint plan is ⟨move(B, SW, CW), move(B, CW, CE), move(R, NE, CE), move(R, CE, CW)⟩ then move(R,NE, CE) will fail as its precondition loc(B) ̸= CE is false when it is executed.

To address such conflicts, previous work [Tenneholtz and Moses, 1989] proposed the concept of SL - a set of restrictions designed to improve coordination among agents. SLs can be applied to multi-agent planning problem [Karpas et al., 2017], where a SL modifies a multi-agent planning setting Π, yielding a new setting ˜Π. This modification may involve removing certain actions [Nir et al., 2020] or adding auxiliary facts that aid in managing agents' behaviors through bookkeeping [Tuisov and Karpas, 2020; Tuisov et al., 2024]. SLs can also implement more complex restrictions using a waitfor mechanism, which holds an agent inactive until a condition f is satisfied before it executes its next action. We denote the waitfor condition of action a by prew(a), while the remainder of the condition of a is denoted by pref (a) (for failure).

To illustrate the concept of waitfor, consider our running example. It makes sense for an agent that is trying to move to some location l2 to wait until l2 is clear before it moves into it.

Thus, we can write prew(move(i, l1, l2))) = {loc(-i) ̸= l2}, meaning that the agent will not move into an occupied cell, but instead wait for the cell to become clear before moving. Note that the plans depicted in Figure 1b may now result in a deadlock, as each agent will wait for the other agent to move. Again, the exact position of the deadlock will depend on the timing of the actions.

A key property to evaluate for any SL is its robustness, which ensures it effectively prevents conflicts between agents, regardless of the plans they choose to execute.

Robustness We say that a planning task is robust if every agent can choose any individual plan, when it plans as if it was the only agent acting in the world, and be guaranteed it will achieve its goal. To formalize this notion we must first define the execution model of our multi-agent setting.

Let {πi}ni=1 be a set of individual plans. The set of possible executions for these plans is defined by considering (a) the state of the world and (b) the position of each agent within its individual plan. The initial state of execution is ⟨I, 1, . . . 1⟩, indicating that the state of the world is I, and all of the agents are at the beginning of their individual plans. We define four special terminal states of execution: Success: all agents have executed their plans, ending in a goal state for each agent; Failure at execution: an agent tried to execute an action with non-waitfor preconditions that are not satisfied; Deadlock: none of the agents in the system can act; and Goal miss: all agents have executed their plans, ending in a non-goal state for some agent.

The possible transitions from a state of execution ⟨s, j1, . . . , jn⟩ are defined by the set of agents which can act at state s, by looking at their waitfor conditions. Denote the next action of agent i by πi[ji] (that is, the action in position ji in plan πi, where we assume πi[ji] = ⊥ if agent i has completed its plan), and denote the set of agents which can act by C = {i | πi[ji] ̸= ⊥, s |= prew(πi[ji])}, that is, agents for which the current state of the world satisfies the waitfor condition of their next action. Note that the set of transitions only looks at waitfor conditions, and not at the full preconditions of the actions.

If there are no agents that can act, meaning C = ∅, we have two subcases. If s |= ∧ni=1 Gi, there is a single transition to Success, indicating that all agents have successfully completed their plans and achieved their goals. Otherwise, if s ̸|= ∧ni=1 Gi, there is either a single transition to Deadlock, as no agents can act, or Goal miss as all agent finished executing their plans.

If agents can still act, there are several possible transitions, one for each agent i ∈ C. Again, we have two subcases. If s ̸|= pre(πi[ji]), meaning the current state of the world does not satisfy the preconditions of the next action of agent i, the resulting state from applying the action of agent i is Failure. Conversely, if s |= pre(πi[ji]), the action is successfully applied, and the resulting state from applying the action of agent i is the execution state ⟨s�πi[ji]�, j1, . . . , ji-1, ji + 1, ji+1, . . . , jn⟩, meaning the state of the world is updated, and the position in πi is incremented by 1.

We can now define robustness: a SL is robust for Π iff for every set of individual plans {πi}ni=1 , every possible execution of these plans results in Success. Coming back to our running example, consider a social law in which (a) an agent does not move into an occupied location (formulated using a waitfor condition, as described above), and (b) agents are only allowed to move in a counter-clockwise direction, formulated by removing the actions which move clockwise from the action sets AR and AB. Figure 1c shows the resulting plans under this SL, and indeed it is possible to show that this SL is robust.

Previous work [Karpas et al., 2017] has shown how to verify whether a given SL in an MA-STRIPS setting is robust. However, it cannot be directly applied to our running example, as (a) it uses finite domain variables, and (b) it employs negation in preconditions. In the next section, we describe a general computational technique for checking the robustness of any SL in any multi-agent setting, which can be directly applied to our running example, and many others.

3 Generalized Compilation

We now describe our contribution - a new technique for verifying the robustness of a given social law. Similarly to previous work [Karpas et al., 2017] this technique relies on creating a planning problem whose objective is to find a counterexample to robustness (that is, a trajectory in the execution model which leads to Failure, Deadlock, or Goal miss). However, the previous work relied on the planning problem being formulated in MA-STRIPS or numeric MA-STRIPS [Nir et al., 2023], while the compilation we present here is directly applicable with instantaneous actions, and for which we can compute the negation of a condition efficiently. Thus, the new compilation is directly applicable to our running example, without having to translate it to MA-STRIPS.

Similarly to the original compilation [Karpas et al., 2017], the new compilation generates n + 1 copies of each variable from the original problem. We label copies 1 through n as local copies (one per agent), while the final copy, denoted by g, is the global copy. The global copy emulates joint execution, whereas the local copies assures that each agent indeed independently plans toward its own goal.

Our compilation operates in two stages. In stage 1, we simulate the execution process, where each agent applies its actions in an order chosen by the planner while respecting waitfor conditions. In other words, stage 1 accounts for the actions actually executed. Once stage 1 terminates, we move to stage 2, which handles bookkeeping - ensuring that the actions executed by each agent in stage 1 form a prefix of an individual plan for that agent (otherwise, agents could execute actions that do not lead to a goal).

In stage 1, an action ai may succeed, fail, or result in a deadlock (waiting forever), which is represented by having 3 different versions of ai applicable in stage 1: asi (success), afi (failure), and awi (wait). Applying asi is possible when the global state satisfies pre(ai), updates the global state with the effects of ai and keeps the compilation in stage 1. Applying afi is possible when the global state does not satisfy pre(ai) but does satisfy prew(ai), raises the precondition violation (PrV) flag, and moves the compilation to stage 2. Following this, the compilation ensures that each agent can reach its goal in its local copy of the state by applying a fourth version of each action, ali , which only updates the local copy of agent i.

Applying the wait action awi is only possible when the global state does not satisfy prew(ai), signaling a potential Deadlock. This means that, from this point onward, agent i cannot execute any action except ai until ai is executed. Executing awi sets a flag that allows agent i to execute only ai, encoded by the condition RAi ∧ allow(ai), but does not update the global state with the effects of ai. After this flag is raised, agent i has two options: either execute ai in both its local and global copies or execute the deadlock action deadlock-ai. If all agents are either in a deadlock state or have completed their plans, stage 1 ends, transitioning the compilation to stage 2. Then, as with afi , the local copies are used for each agent to achieve its goal separately.

We also allow the search to continue to stage 2 once all agents have achieved their goals. The goal of the compilation is a fact conflict which signals that either a deadlock or a precondition violation occurred. This is achieved by declare-deadlock, which checks that a deadlock occurred or declare-fail, which checks that a precondition violation occurred by execution of some afi . Finally, it may be the case that all agents have finished their respective individual plans with no interruption, but the goal of some of them is not achieved at the end of the execution. We check for this condition using the goals-not-achieved action, which performs a straightforward check. The goal flag conflict is achieved only by these three actions. We now describe the full details of our compilation, and then proceed with proving its correctness.

3.1 Full Compilation

We define Π′ = ⟨V ′ ,A′ , I ′ ,G′ ⟩ to be the compiled planning problem. A solution for Π′ represents a conflict in the multiagent problem Π. We start with defining Vi = {vi | v ∈ V} to be the variables of each local copy i ∈ [n], and Vg = {vg | v ∈ V} to be the variables of the global copy, with dom(vi) = dom(vg) = dom(v). In addition, we define the following set of auxiliary flags, each with a Boolean domain:

Using this notation we define the variables of Π′ to be V ′ = Aux∪Vg ∪ ⋃i∈[n] Vi. Also to ease the notation, for each flag flag we use the following shorthand: flag = ⊤ is replaced with flag and flag = ⊥ with ¬flag, this holds for both assignments and equalities. Since all the conditions in the set must hold true, each set of conditions can be written as X = ∧f∈X f , using the same notation ¬X = ∨f∈X ¬f .

We continue with the actions of Π′ . For each set of formulas X over the variables in V, we denote by Xi and Xg the same set of formulas but written over the variables in the copies Vi and Vg, respectively. This applies to both sets of conditions such as pre(ai) or Gi are mapped into conditions prei (ai) and preg (ai) and Gii and Ggi , respectively. The goal of the global copy is denoted Gg := ∧ni=1 Ggi . Note that each agent i affects only its copy i, the global copy g or both. The same notation also applies to the effects of each action ai, which are applied to the the copy of the agent i and global copy g. For each action in Ai we define five distinct copies:

Of these, three change the local copy of the agent - asi , afi , ali . These actions also do the following: asi is the successful action that changes the global copy where all agents act in stage 1, afi indicates failure due to precondition violation and stops the execution in the global copy ending stage 1 and indicating failure, and the action ali that assures that each agent still achieves its goal in its local copy. Formally they are defined as follows:

• pre(asi ) = stage1 ∧ (allow(ai) ∨ ¬RAi) ∧ prei (ai) ∧ preg (ai),

• pre(afi ) = stage1 ∧ (allow(ai) ∨ ¬RAi) ∧ prei (ai) ∧ pregw (a) ∧ ¬pregf (ai),
• eff(afi ) = {P rV, stage2, ¬stage1} ∪ effi(ai),
• pre(ali ) = stage2 ∧ (allow(ai) ∨¬RAi) ∧ prei (ai), add(ali ) = eff i (ai) ∪ {allowai , ¬RAi};

The actions awi and deadlock-ai are actions that manage waiting, where the first action indicates that agent i is waiting to execute action ai, and the second indicates that a potential deadlock has occurred. Formally:

• pre(awi ) = stage1 ∧ allow(ai) ∧ prei (ai) ∧¬preiw (ai), eff(awi ) = ⋃a∈Ai\{ai} {¬allow(a)} ∪ {RAi};
• pre(deadlock-ai) = allow(ai) ∧¬pregw (ai) ∧RAi, eff(deadlock-ai) = {f ini, P oD, ¬stage1};

We also have auxiliary actions: end-successi is applicable if the agent achieves its goal in both the local and global copies. Another action initiates stage 2, where each agent pursues its goal in the local copy. Three additional actions conclude the plan with failure.

{declare-deadlock, declare-fail, goals-not-achieved}.

Below we present these actions in detail:

• pre(end-successi) = Ggi , eff(end-successi) = {f ini, ¬stage1};
• pre(start-stage2 ) = ∧i∈[n] fini, eff(start-stage2 ) = {stage2, ¬stage1};
• pre(goals-not-achieved) = stage2 ∧¬Gg ∧ ∧ni=1 Gi , eff(goals-not-achieved) = {conf lict};
• pre(declare-deadlock) = stage2 ∧PoD∧ ∧ni=1 Gi , eff(declare-deadlock) = {conflict}; and
• pre(declare-fail) = stage2 ∧ PrV ∧ ∧ni=1 Gi , eff(declare-fail) = {conf lict}.

In the initial state we set all the copies to emulate the initial state of Π and declare that the agents currently in stage 1:

all flags other than stage1 are set to false. The goal is to achieve conflict, i.e., G′ = {conflict}.

Compilation Example To better understand the compilation, we present the solution to the compilation in our running example under several different possible social laws. For the original setting without any social laws, recall the agents can crash into each other. One possible solution for the compilation (the same one explained above) is: ⟨move(B, SW, CW)s , move(B, CW, CE)s ,

move(R,NE, CE)f ,move(R, CE, CW)l , declare-fail⟩. Note that the third action in this solution is the one in which R moves into a cell already occupied by B, violating one of the preconditions, which is why we can use the the af version of the action.

Now consider the social law where we turn this violated precondition into a waitfor condition, meaning that an agent will wait rather than moving into an occupied cell. In this case, we can get a different solution to the compilation resulting in a deadlock: ⟨move(B, SW, CW)s , move(B, CW, CE)s ,

move(R, NE, CE)w , deadlock-move(R, NE, CE)w ,

move(R, CE, CW)l , declare-deadlock⟩. Finally, if we also add the restriction of only moving counter-clockwise (meaning the above solution is no longer possible, as B and R move clockwise in it), our compilation yields an unsolvable planning problem - proving that this social law is robust.

3.2 Proof of Correctness

We formally prove the correctness of our compilation in three steps. First, we establish a correspondence between executions in the original task and plans that solve the compiled task. Second, we demonstrate that if the compiled problem is solvable, the underlying problem is not robust. Finally, we prove the converse: if the underlying problem is not robust, then the compiled task is indeed solvable.

Let Π = ⟨V, {Ai}ni=1 , I, {Gi}ni=1 ⟩ denote the original problem, and let Π′ = ⟨V ′ ,A′ , I ′ ,G′ ⟩ be the compiled problem as described in Section 3.1. We use a prime notation when referring to elements of Π′ if the context might be ambiguous; for instance, π′ denotes a plan that solves Π′ .

Our goal is to provide the connection between the interleavings of agents' individual plans in Π and the plans of the compiled problem Π′ .

Observation 1. Every plan π′ solving Π′ must end with either goals-not-achieved, declare-deadlock or declare-fail actions. All of these have stage2 as their preconditions and no action deletes stage2. Moreover, the initial state I ′ includes stage1, no action adds stage1, and every action that adds stage2 deletes stage1 (but not vise versa, some actions delete stage1 without adding stage2). Thus any π′ will include a unique action a′i deleting stage1, a unique a′j that adds stage2 and it is guaranteed that i ≤ j. This means, it is always possible to split π′ into a prefix pref(π′ ), a (possibly empty) infix inf(π′ ), and a suffix suf(π′ ), where the prefix ends with a′i (ending stage1), and the suffix starts with a′j+1 (starting stage2).

We establish a correspondence between executions in Π and plans for Π′ .

Definition 1 (Equivalent sequence and execution). Let π′ be a plan for the compiled problem Π′ . Define π[n] to be an equivalent execution of π′ as a restriction of pref(π′ ) to the variables in Vg = {vg | v ∈ V}. Note that since awi does not affect Vg it can be safely removed from consideration.

Let π[n] = (a1, . . . , am-1, am) be an execution of the individual plans {πi}ni=1 in the multi-agent task Π. Define eq(π[n] ) an equivalent sequence of π[n] in the compilation Π′ to be (as1 , . . . , as(m-1) ) if execution fails, otherwise (as1 , . . . , asm).

The equivalent sequence of a valid execution is always sequentially applicable in Π′ , since Vg and every Vi = {vi | v ∈ V } are copies of V, effects of any action a on V are identical to effects of as on Vg, and the effects of any ai are identical to the effects of asi on Vi. This means that the state of V and every Πi after executing some π[n] is identical to the state Vg and every Vi respectively after executing eq(π[n] ).

Our goal it to show that for every failed execution π[n] in Π there is a plan π′ for Π′ , and vice versa. More formally:

Theorem 1 (The correctness of the compilation). Given a multi-agent task Π = ⟨V, {Ai}ni=1 , I, {Gi}ni=1 ⟩ and the complied single agent task Π′ = ⟨V ′ ,A′ , I ′ ,G′ ⟩, Π′ is solvable if and only if Π is not robust.

Proof is by the combining the following two lemmas.

Lemma 1. π[n] is a failed execution =⇒ Π′ is solvable.

Proof. Assume π[n] is a failed execution. We want to construct a corresponding plan π′ for Π′ . This means that π is applicable in the initial state I ′ and achieves G′ = {conflict}. To construct π′ , it is sufficient to specify pref(π′ ), inf(π′ ), and suf(π′ ).

By construction of V ′ , eq(π[n] ) is consecutively applicable in Π′ . Since pref(π′ ) includes all actions in π′ executed in stage1, we have that eq(π[n] ) is a prefix of pref(π′ ). Failed execution π[n] implies that individual plans {πi}ni=1 ended either with Missing the goal ∧ni=1 Gi, in a Failure, or in a Deadlock. For each agent i, either πi is a subsequence of π[n] , which means i had finished its execution by the end of π[n] , or πi is not a subsequence of π[n] .

Denote the set of all agents that finished their execution as FINISHED(π[n] ) and define NOT-FINISHED(π[n] ) := [n] \ FINISHED(π[n] ). In a case when NOT-FINISHED(π[n] ) ̸= ∅, we call the suffix of πi that does not appear in π[n] an unexecuted suffix of i. By γ l we denote some arbitrary interleaving of unfinished suffixes for all i ∈ NOT-FINISHED(π[n] ). Note that γ l are executed in local copies of the appropriate agents and therefore the order of agents is not important. The sequence of actions γ l is the part of suf(π′ )

We aim at reconstructing a plan π′ , such that eq(π[n] ) is the prefix of π′ . We also introduce the following notation for plan reconstruction purposes: x ∥ y stands for concatenation of action sequences x and y. Consider three cases:

Case 1 (Goal miss): ∧ni=1 Gi is not achieved after executing π[n] and neither failure nor deadlock occurred. Since eq(π[n] ) is the equivalent sequence of π[n] the global copy variables in the states in Π′ correspond to the states of Π, we know that after the execution of π[n] , the condition ∧i∈[n] Ggi =

∧i∈[n] ∧f∈Gi fg was not achieved. And since all agents have finished their executions the local copy goals Gii := ∧f∈Gi fi were achieved for each i.

Hence, the plan π′ looks as follows: pref(π′ ) = eq(π[n] ), inf(π′ ) = (∥∥i∈[n] end-successi) ∥ start-phase-2, suf(π′ ) = goals-not-achieved. Note that the application of the actions end-successi can be done in any order, thus any predefined order will do. π′ is valid since the actions are consecutively applicable, and conflict is true in the final state.

Case 2 (Failure): π[n] ends in a failure. Denote the action failing as aα. The full plan π′ will look as follows: pref(π′ ) = eq(π[n] ) ∥ aα, inf(π′ ) = ∅, suf(π′ ) = γ l ∥ declare-fail. This plan is valid because after applying eq(π[n] ), global preconditions of aα are not satisfied by equivalence of eq(π[n] ). Local preconditions of aα, however, are satisfied because otherwise aα could not be picked to be the next action performed in Π. At the end of eq(π[n] ) the local executions continue. The local actions are executable in arbitrary order since the local copies have no effect on each other, and after their execution it necessarily holds that Gii := ∧f∈Gi fi is satisfied for each i, otherwise πi would not be a plan in Πi.

Case 3 (Deadlock): π[n] ends in a deadlock. This means, every agent had either finished its execution or waiting for some waitfor precondition to become true. Then π′ will look as follows: pref(π′ ) = eq(π[n] ) ∥ (∥∥i∈NOT-FINISHED(π[n] )awi ) where ai is the first action in the unexecuted suffix for each i;

and suf(π′ ) = γ l ∥ declare-deadlock, where all the actions end-successi and deadlock-ai are executed in arbitrary order.

This plan is valid because after executing π[n] , we know that every i ∈ NOT-FINISHED(π[n] ) was waiting for some waitfor precondition to become true. Thus, after applying eq(π[n] ), for each i ∈ NOT-FINISHED(π[n] ) there will be such an ai that its regular preconditions are met, but waitfor preconditions are not. Thus, awi are applicable, and can be applied in arbitrary order since they have no effect on each others preconditions. After that, deadlock-ai actions become applicable. As soon as one is applied, stage1 is deleted, and no actions but the deadlock-ai, end-successi, and start-stage2 are applicable. To achieve fini for all i ∈ [n], deadlock-ai is performed for waiting agents, and end-successi is performed for finished agents, again in arbitrary order. After that, start-stage2 , and, subsequently local actions become applicable. The local actions are executable in arbitrary order since they have no effect on each other, and after their execution it is necessary that ∧f∈Gi fi is satisfied for each i, otherwise, πi would not be a plan in Πi.

Proof. Let π′ be a plan for Π′ . We need to show that there is a set of individual plans {πi}ni=1 such that their interleaving execution π[n] is not a joint plan. In other words, π[n] ends in either Goal miss, Failure, or Deadlock.

The plan π′ restricted to local copies of each agent variables Vi = {vi | v ∈ V}. The only actions that have effect on local copy i are asi , afi and ali , thus to reconstruct individual plan for agent i every other action can be safely removed from consideration. The remaining actions corresponds to some individual plan πi, since the plan π′ should achieve local goals of each agent to achieve the conflict goal in Π′ .

Note that π′ defines the waitfor-respecting order of execution of the individual plans {πi}ni=1 . Define π[n] to be the stage1 subsequence of actions in π′ restricted to the original actions that correspond to asi and afi . Note that we ignore the waiting actions of the form awi since these actions change only the flags, but not the copies of the original variables.

From Observation 1 we know that π′ includes either goals-not-achieved, declare-fail or declare-deadlock actions. We distinguish between these cases, since they define the nature of the executions failure:

Case 1 (Goal miss): π′ includes goals-not-achieved. By construction, this means that a goals-not-achieved flag was raised. This is only possible if every fini was raised, but some goal was not achieved in the global copy. By equivalence of π′ and π[n] , at the end of π[n] some global goal will not be achieved as well.

Case 2 (Failure): π′ includes declare-fail. By construction, the precondition-violation flag was raised, thus some action afi was applied, and it was the last action in pref(π′ ) since every afi deletes stage1 flag. By equivalence of π′ and π[n] , at the last step of the execution action ai was not applicable, thus its application would result in a failure. Moreover, every ai is performed in an individual plan πi. Such πi is a subsequence of π′ restricted to agent i, where each ai ∈ πi has its source in asi , afi or ali , respectively. It is guaranteed that such πi exists because π′ has to achieve ∧ni=1 Gi in the local copies to apply declare-fail.

Case 3 (Deadlock): π′ includes declare-deadlock. By construction, the possible-deadlock flag was raised, thus at least one action deadlock-ai was applied. This means that action start-stage2 was applied, because deadlock-ai and afj for any agent i, j are mutually exclusive, since both require and remove the stage1 flag. The start-stage2 action requires performing either end-successi or deadlock-ai for each i. Since there are no failures, either end-successi or deadlock-ai were used. This means no agent i can apply a successful action, because it either has achieved its goal or is in a deadlock. The action end-successi requires ∧f∈Gi fi, which means in the equivalent π[n] agent i has achieved its goal and stopped the execution. The action deadlock-ai requires both RAi and ∧ ∨f∈prew (ai) ¬fg. The first requirement means that the previous action of agent i was awi since otherwise actions in Ai \ {ai} would not be disallowed. The second requirement ensures that no action of the type as , not even asi can be performed. Hence, during π[n] agent i waits for some precondition to become true. Thus, every agent i is either finished or waiting, meaning that π[n] results in a deadlock.

4 Experimental Evaluation

The compilation presented above is more general than the earlier approaches [Karpas et al., 2017; Nir et al., 2023], but this increased generality might lead to more challenging planning problems. To evaluate this trade-off, we conducted an empirical study, comparing the solving times for problems generated by our compilation (new) and the previous one (old). We do not employ the numeric compilation by Nir et al. [2023], since it requires manual problem adjustment.

Both compilations were implemented 1 on top of the Unified Planning Framework [upf, 2025], and all of our benchmarks were encoded in this framework. Classical problems were grounded using the Fast-Downward grounder [Helmert, 2006]; the planner used for both compilations was the LAMA-first planner since it is the baseline/winner of the last IPC 2023 Agile Track [Taitler et al., 2024]. Numeric problems were solved by ENHSP-20 [Scala et al., 2020]. The planners had a time limit of 30 minutes on an Intel i7-6700k CPU, and a memory limit of 8GB for Fast Downward and 16GB for ENHSP. We measure the time it takes to solve the resulting planning problems from both compilations.

We performed the comparison on a set of benchmarks adapted from the first Competition of Distributed and Multiagent Planners [Stolba et al., 2015] and from the Numeric track of IPC 2023 [Taitler et al., 2024] described below:

GRID: each agent starts at a randomly assigned point and navigates toward a designated finish point to exit the map. The experiments examine movement with and without a social law. Under the social law, agents follow directional rules: they move in a circular pattern along grid borders and alternate upward and downward in inner columns, similar to a warehouse layout. The law prevents collisions by requiring agents to wait for spaces to be clear before entering them. There are both classical and numeric versions of this domain.

1 Code available at https://github.com/ TechnionCognitiveRoboticsLab/up social laws ijcai2025

ZENOTRAVEL: aircraft transport individuals between cities, consuming varying fuel amounts and with the option to refuel, where each aircraft acts as an agent. Individuals board and disembark from aircraft to reach their destinations. A robust social law assigns individuals to the aircraft that is responsible for delivering them to their destinations. here is both classical and numeric version of this domain.

BLOCKSWORLD: robotic arms act as individual agents that pick up and stack blocks. While agents can independently reach their own goals, cooperation is needed for collective objectives. For instance, if agent 1's goal is ON(A,B) and agent 2's goal is ON(B, C), they need a three-block tower to satisfy both goals, requiring coordination beyond individual efforts. An effective social law to ensure such cooperation is yet to be identified.

DRIVERLOG: Drivers travel on foot or by truck, loading or unloading packages to reach targets. Each driver manages specific packages and, at most, one truck. A robust SL is unworkable because truckless drivers depend on borrowing and returning trucks, creating dependencies that prevent fully independent problem-solving.

MARKET TRADER: In this trading scenario, agents (camels) travel between markets to buy and sell goods, balancing costs, availability, and capacity. Actions include traveling, purchasing, upgrading capacity, and selling for profit. The goal is to maximize cash through strategic resource allocation. Instances were adjusted by reducing the number of goods to ensure solvability by existing planners.

EXPEDITION: In this domain, agents (sleds) navigate between waypoints in a network. Sleds consume supplies to travel between adjacent waypoints. Supplies can be stored at or retrieved from waypoints, constrained by sled capacity. The objective is to manage supplies efficiently while traversing the network.

Table 1 shows results for each domain without the SL, and with the SL when one is available. new denotes the compilation in this paper, while old is a compilation for MA-STRIPS presented by [Karpas et al., 2017]. The table presents coverage and the geometric mean of running time (in seconds) for the problems that were solved both by old and new compilations. For numeric multiagent domains we present the (geometric) mean time of the problems solved by the new compilation. The tables also show that while the new compilation is slightly slower, it is able to verify two more instances with SL in the classical ZENOTRAVEL, and finds one less counter example in DRIVERLOG. Exact runtimes for each problem are available in the supplementary material.

5 Conclusions

We introduced a novel compilation for verifying the robustness of social laws in multi-agent planning scenarios, which is more general than previous methods, accommodating both classical and numeric planning formalisms. Despite its broader applicability, the proposed method demonstrates state-of-the-art performance.This advancement not only enhances the verification process but also lays the groundwork for integrating social laws into richer planning frameworks, opening new possibilities for research in multi-agent systems.

Acknowledgements

Alexander Shleyfman's work was partially supported by ISF grant 2443/23. Work also supported by a grant from the Trudy Lewis Foundation and the Israeli Planning and Budgeting Committee of the Council for Higher Education.