Synthesising Minimum Cost Dynamic Norms

1 Introduction

In normative multi-agent systems, system-level objectives are realized through norms [Chopra et al., 2018]. A norm expresses a pattern of desired or undesired behaviour that achieves or violates a system objective. For example, a norm may specify that it is not permitted to travel on public transport without valid ticket (to ensure the financial viability of the transport authority), or to smoke in a public place (to reduce the health risks to others), etc.

A key problem in the design of normative multi-agent systems is the cost of enforcing or complying with the norm. Enforcing norms typically has a cost to the system (normative organisation), e.g., the cost of installing ticket barriers to control access to a public transport system. Different actions may be more or less costly to control, e.g., it may be more costly to control access to an open-air concert than to a metro station. Complying with a norm also has a cost (loss of utility) for agents which may be different for different agents; for example, a norm prohibiting smoking in public places may result in no loss of utility for an agent who does not smoke, but a significant loss of utility for an agent who does smoke. If the costs are too high, ensuring compliant behavior may be uneconomic, or users may be deterred from participating in the MAS.

While the implementation of norms in a MAS has been extensively studied, e.g., [Meyer and Wieringa, 1993; Grossi et al., 2006; ˚Agotnes et al., 2007; Astefanoaei et al., 2009; Dennis et al., 2010; Dastani et al., 2013; ˚Agotnes et al., 2010; Bulling et al., 2013; Dignum et al., 2004; Boella and van der Torre, 2004; Boella et al., 2008; Tinnemeier et al., 2009; Alechina et al., 2013], there has been less work on how norms can be automatically synthesized to meet an objective. Synthesis of norms was first introduced in [Shoham and Tennenholtz, 1995], and also studied in [Fitoussi and Tennenholtz, 2000; Christelis and Rovatsos, 2009; Corapi et al., 2011; Morales et al., 2015a; Morales et al., 2018]. In the context of logical objectives, norm synthesis has been studied in, for example, in [van der Hoek et al., 2007; Bulling and Dastani, 2016; Huang et al., 2016; Perelli, 2019; Alechina et al., 2022]. However, with the exception of [Perelli, 2019] where a related problem of norm optimization was introduced, this work has not considered the cost of the synthesized norm(s).

In this paper, we consider the problem of synthesizing minimum cost dynamic norms to satisfy a system-level objective specified in Alternating Time Temporal Logic with Strategy Contexts (ATL∗sc ). We focus on dynamic norms [Huang et al., 2016], as these are more flexible than 'static' (state based) norms in allowing constraints to be enforced on the actions of agents based on their history of interaction with the MAS. For example, in the interests of fairness, a normmay specify that if an agent was previously prohibited from performing an action, it should be allowed to perform the action in the current state. Our notion of the cost of prohibiting an action is quite general, in the sense that it admits any assignment of costs to prohibiting sets of actions, and can express both the loss of utility to the agents and/or the cost of enforcing the norm to the normative organisation. For example, if all actions have the same cost, a minimum cost norm can be seen as "maximally permissive", i.e., it prohibits the minimum number of actions necessary to achieve the system objective. On the other hand, if agents place greater value on being able to perform some actions than others, a minimum cost norm may be one that maximizes social welfare while achieving the objective. We use ATL∗sc to express system objectives as this allows us to specify the strategic abilities of (groups of) agents in the MAS, both to state that a particular group of agents should (or should not) be able to achieve a particular goal, as well as stating that given the individual goals of agents, there is a Nash equilibrium. We consider norm synthesis for two natural notions of norm cost, maximum single step cost and average step cost. The maximum single step cost is the maximum cost of any prohibited set of actions and is relevant when the system designer wishes to minimise the maximum loss of utility/cost of enforcement incurred due to a norm. The average step cost is the average cost of the prohibited set of actions over an infinite run and and is relevant when the aim is to minimise the average loss of utility/cost of enforcement resulting from the norm. Both notions are useful depending on the context: for example, a short lockdown during a pandemic may have a high maximum single step cost (impacting individual liberties), but low average step cost (impacting economic activity). We show that synthesizing a dynamic norm under a bound on the maximum single step cost has the same complexity as synthesizing arbitrary norms in [Alechina et al., 2022] (i.e., (h + 1)-EXPTIME for an existential ATL∗sc formula with quantifier alternation number h, and in (h+2)-EXPTIME for a universal ATL∗sc formula). We also show that synthesizing a dynamic norm that minimizes the average step cost does not always have a solution as it requires infinite memory. However, synthesizing ϵ-optimal norms is possible for a restricted class of ATL∗sc objectives.

2 Framework

In this section we introduce the definitions needed to formalise reasoning about dynamic norms in multi-agent systems, largely following [Alechina et al., 2022].

2.1 SystemModels

We assume a multi-agent system coordinated by zero or more dynamic norms, which we formalize as a particular kind of game.

Definition 1 (k-normed Multi-Agent System). A knormed Multi-Agent System (k-MAS) G is a tuple ⟨Ag, Ac, AP, Cap, tr, (Nrmi)i≤k, ⃗q0, (ηi)i≤k, (illegali)i≤k⟩ where:

• Ag = {1, . . . , N} is a finite set of N agents, denoted by natural numbers;
• Ac is a finite set of actions that agents can perform (in some state of the environment);
• AP is a finite set of atomic propositions; an assignment of truth values to AP determines environment states of the system;
• Cap : Ag × 2AP → 2Ac is a capability function that assigns to each agent in each environment state the set of actions it is capable of performing in that state
• tr : 2AP ×AcAg → 2AP is a transition function that determines the next state of the environment given the current state of the environment and the actions performed by the agents;
• Nrmi is a finite set of normative states, one for each i ≤ k; ⃗ Nrm = Nrm1 × . . . × Nrmk, is the normative vector state space (the set of tuples containing the state of each norm);
• ⃗q0 ∈ ⃗ Nrm is a designated initial normative state;
• ηi : Nrmi × 2AP → Nrmi is a normative function that determines the next state of a norm given the current state of the norm and the environment;
• illegali : Nrmi ×2AP → 2Ac-×Ag is the illegality function that returns a set pairs of actions and agents that are illegal given the current state of a norm and the environment.

Unlike [Alechina et al., 2022], we assume that there is a distinguished action noop ∈ Ac which is always available to every agent and is never illegal, i.e., intuitively it is always possible for an agent to do nothing. We denote by Ac- the set Ac \ {noop}. This change does not affect the results in [Alechina et al., 2022].

We illustrate a k-MAS with a simple example of a normative multi-agent system.

Example 1 (k-MAS). Consider a traffic intersection with two agents. Agent 1 moves North-South and agent 2 moves EastWest. Each agent has two actions, go and noop. AP = {east, west, north, south, crash}. Intuitively, east holds when agent 2 is in the East, etc. The action noop does not change an agent's position; go moves agent 1 from North to South or back, and agent 2 from East to West or back (if the other agent does noop); go, go results in a crash. The initial state is when agent 1 is in the North and 2 is in the East. There is one norm (k = 1) with two states, q1 and q2, which alternate (on any input). For any state of the environment, in q1 there is a single illegal action (go, 2) and in q2 there is a single illegal action (go, 1). The initial norm state is q1. The norm acts as a traffic light, allowing only one agent to move at every step. The states of the norm can be seen as encoding the history in the game so far and hence whose turn it is to go at the current step.

Evolution Starting from some initial state of the environment (a set of atomic propositions) π0 and the initial vector of normative states ⃗q0, a game moves forward according to the transition function, which given the current state of the environment and an action tuple ⃗a ∈ AcAg , determines the next state of the environment (assignment to the propositions in AP). Simultaneously, each normative component is updated by the corresponding normative function, which, given the current state of the norm and the current environment state, determines the next state of the norm.

Configuration, Illegal Actions, Available Actions A configuration of G is a tuple c = (π,⃗q) ∈ 2AP × ⃗ Nrm (a tuple consisting of the state of the environment and the states of the norms). The set of actions that are made illegal for agent j by the i-th normative component is denoted by illegali(qi, π, j) .= {a ∈ Ac : (a, j) ∈ illegali(qi, π)}. The set of actions available to agent j in configuration c, where ⃗qi is the i-th component of ⃗q, is denoted by AvlG(c, j) .= Cap(j, π) \ (∪i≤killegali(qi, π, j)). The set AvlG(c) .= AvlG(c, 1) × . . . × AvlG(c, N) denotes the action vectors that are available in a configuration c.

In Example 1, the initial configuration is ({north, east}, q1), and agent 1 has actions go, noop available, while agent 2 only has available action noop, since (go, 2) is illegal.

At each configuration c = (π,⃗q), each agent j can select only an action aj ∈ AvlG(c, j). Once each agent j has chosen an available action aj and the corresponding action vector ⃗a = (a1 , . . . , ak ) is formed, the systemmoves its components forward to the configuration (π′ ,⃗q′ ), with π′ = tr(π,⃗a) and ⃗q′ = (η1(q1 , π), . . . , ηk(qk , π)).

Runs of the system A legal run, or simply run is an infinite sequence r ∈ (2AP × ⃗ Nrm)ω such that, for each n ∈ N, there exists an action vector ⃗an ∈ AvlG(rn), such that

with rn = (πn,⃗qn). We use the notation r≤n to denote the prefix of r up to and including rn. Similarly, r≥n is the suffix of r starting from rn. c ⃗a-→ c′ is used to denote that the action vector ⃗a determines a transition from configuration c to configuration c′ . A run is initial if it starts from the initial configuration, that is, r0 = (π0,⃗q0).

A possible run of the system in Example 1 is ({north, east}, q1), ({south, east}, q2), ({south, east}, q1), ({north, east}, q2), . . . where agent 1 executes go whenever it can, and agent 2 always executes noop even when go is available.

Strategy A strategy for agent j in the game G is a Mealy machine of the form

For each internal state s ∈ Sj and a configuration c = (π,⃗q) of G, a strategy selects an action in Ac determined by τj(s, (π,⃗q)) ∈ Ac and updates its internal state δj(s, (π,⃗q)) ∈ Sj accordingly. Only the strategies that comply with the normative requirements specified by the game are available to the agents. A strategy σj is legal with respect to G if, and only if, τj(s, (π,⃗q)) ∈ Avl(⃗q, π, j). From now on, we restrict our attention to legal strategies, and, unless otherwise stated, we refer to them simply as strategies. Moreover, for simplicity, for a given strategy σj and a finite sequence ˆ r ∈ (2AP × ⃗ Nrm)∗ , by σj(ˆ r) ∈ Ac we denote the action determined by the function τj in σj after the sequence ˆ r has been fed to the internal transition function δj.

A simple strategy for agent 2 would be to always execute noop. This requires a Mealy machine with a single state, that on any input returns noop and loops back to the same state. A strategy for agent 1 would be executing go on input of q1 (regardless of the state of the world, that is, of the propositional assignment), and noop on input of q2.

Note that the restriction to regular strategies representable by Mealy machines is without loss of generality, as when the specification language is ω-regular, synthesizing a strategy satisfying the specification is equivalent to synthesizing a regular strategy [Pnueli and Rosner, 1989].

Runs compatible with strategies A run r is compatible with σA (where A is a set of agents) if, for every n ∈ N, it holds that there exists an action vector ⃗an, with ajn = σj(r≤n) for each j ∈ A and σj ∈ σA, such that rn+1 is obtained from rn by applying ⃗an. In other words, a run r is compatible with σA if it can be generated when the agents in A play according to their respective strategies. The set of runs starting from a given configuration c and compatible with σA

is denoted by outG(c, σA). Observe that the set of runs of a given k-MAS G starting from a configuration c, sometimes denoted PathsG(c), can also be written as outG(c, ∅). When it is clear from the context we use Paths(c) or out(c, σA).

2.2 ATL∗sc- Alternating-Time Temporal Logic with Strategy Contexts

We use an extension of Alternating-Time Temporal Logic (ATL∗ ) [Alur et al., 2002], Alternating-Time Temporal Logic with Strategy Contexts (ATL∗sc ) introduced in [Da Costa Lopes et al., 2010] to express system objectives. We refer the reader to [Laroussinie and Markey, 2015] for a detailed discussion of ATL∗sc .

ATL∗sc formulas are built inductively from the set of atomic propositions AP and agents Ag. There are two types of ATL∗sc formulas, state formulas and path formulas. State formulas are built by using the following grammar, where p ∈ AP, A ⊆ Ag and ψ is ATL∗sc path formula:

Path formulas are built using the following grammar, where ϕ is a state formula of ATL∗sc :

We also use the following syntactic sugar notation: φ1 ∨ φ2 .= ¬(¬φ1 ∧ ¬φ2), φ1 → φ2 .= ¬φ1 ∨ φ2, [·A·]φ .= ¬⟨·A·⟩¬φ, Fφ .= trueUφ, and Gφ .= ¬F¬φ.

Formulas of ATL∗sc are evaluated relatively to a strategy context: a fixed strategy σB for a group of agents B. The formula ⟨·A·⟩ψ means that the agents in A have a collective strategy such that whatever the agents Ag \ A do (provided the strategies in σB are fixed), the resulting outcomes satisfy ψ. Conversely, the formula ⟩·A·⟨ψ means that whenever the strategies for agents in coalition A are removed from σB, the resulting outcomes satisfy ψ. (Note that the strategy quantifier of ATL∗ can be defined as ⟨⟨A⟩⟩ .= ⟩·Ag·⟨ ⟨·A·⟩.) In addition, the formula [·A·]ψ means that the agents in A do not have a strategy to prevent ψ given σB is fixed for agents in B.

For a given k-MAS G, a run r over it, and a strategy context σB, the semantics of an ATL∗sc path formula ψ, denoted G, r |=σB ψ, is given recursively as follows:

• G, r |=σB ϕ iff G, r0 |=σB ϕ, where ϕ is a state formula;
• G, r |=σB ¬ψ iff G, r ̸|=σB ψ;
• G, r |=σB ψ1 ∧ψ2 iff G, r |=σB ψ1 and G, r |=σB ψ2;
• G, r |=σB Xψ iff G, r≥1 |=σB ψ;
• G, r |=σB ψ1Uψ2 iff there exists j ∈ N such that G, r≥i |=σB ψ1, for all i < j, and G, r≥j |=σB ψ2.

The semantics of an ATL∗sc state formula ϕ is defined relative to a state ri on a run r as follows (we omit the cases for ¬ and ∧ as they are obvious):

• G, ri |=σB p iff p ∈ πi, with ri = (πi,⃗qi) for some ⃗qi ∈ ⃗ Nrm;

• G, ri |=σB ⟨·A·⟩ψ iff there is a strategy σA such that G, r′ |=σB◦σA ψ for all r′ ∈ out(r0, σB ◦ σA), where σB ◦ σA .= σB ∪ σA\B denotes the set of strategies obtained from σB by adding strategies of σA that are for agents in A but not in B.

In Example 1, a simple objective is

It states that agent 1 has a strategy to avoid a crash and to be always able to cross from North to South and back again. In the system in Example 1, such a strategy exists because of the presence of the norm that stops agent 2 from executing go at every other step (so agent 1 can execute go without causing a crash). Without the norm, however, agent 1 alone cannot ensure both the absence of crashing and being able to cross.

The objective above can be expressed in ATL∗ . However, ATL∗sc is more expressive, and can specify useful objectives that are not expressible in ATL∗ , for example, the existence of Nash equilibrium. If each agent j ∈ Ag has a goal expressed by a temporal formula ψj, the existence of Nash equilibrium can be expressed as ⟨·Ag·⟩(∧j∈Ag (¬ψj → ¬⟨·j·⟩ψj)) (see [Laroussinie and Markey, 2015]; the formula says that there exists a joint strategy such that if j's goal is not satisfied, then no deviation from this strategy satisfies it).

The model-checking problem for ATL∗sc is: given a structure G, a run r, a strategy context σB and an ATL∗sc formula φ, does it hold that G, r |=σB φ? The complexity of ATL∗sc model-checking depends on the nesting of quantifiers in a formula, and in particular on how many times existential quantifiers alternate with universal quantifiers. The quantifier alternation number of a ATL∗sc formula φ is the number of times an existential quantification ⟨· · ·⟩ is followed by a universal one [· · ·], and vice-versa.

Theorem 1. [Laroussinie and Markey, 2015, Corollary 14] The model-checking problem for ATL∗sc is (h+1)EXPTIMEcomplete for a formula with quantifier alternation number h.

Although this result was established for concurrent game structures (essentially, 0-MAS without normative components), it also holds for k-MAS because every k-MAS corresponds to a concurrent game structure of size polynomial in the size of the k-MAS, however exponential in k, that is the number of normative components.

2.3 Norms

As in [Alechina et al., 2022], we define a Norm over a k-MAS G as a Mealy machine of the form: N = ⟨Nrm, q0, 2AP, 2Ac×Ag , η, illegal⟩. A norm takes an environment state as input and returns a set pairs of actions and agents that are illegal given the current state of a norm and the environment. N is well-defined on every k-MAS G having the same set Ag of agents, Ac of actions and AP of propositions.

Consider a norm Nk+1 whose components are all indexed with k + 1. Nk+1 can be implemented on a k-MAS G to obtain a (k + 1)-MAS G ⊕ Nk+1 = ⟨Ag, Ac, AP, Cap, tr, (Nrmi)i≤k+1,⃗q0, (ηi)i≤k+1,

(illegali)i≤k+1⟩ containing an extra normative state component, which are the states of Nk+1, and whose evolution is determined by the normative function ηk+1.

For every configuration c in the original game and its extension c′ with the state of Nk+1, it holds that AvlG⊕Nk+1 (c′ , j) ⊆ AvlG(c, j) for every agent j ∈ Ag. Intuitively, Nk+1 introduces more restrictions on the actions for the agents when implemented in a given k-MAS G. Note that all norms allow the agents to perform at least noop, so there will always be an action available to each agent regardless of how many norms we combine.

Observe also that every normative state component i of a k-MAS G can be regarded as a norm Ni = ⟨Nrmi, ei0 , 2AP, 2Ac×Ag , ηi, illegali⟩ and so G can be obtained from a 0-MAS where the norms N1 . . . , Nk have been applied one by one. The norm synthesis problem is as follows (where |=∅ means true in an empty context).

Definition 2 (Norm Synthesis). For a given k-MAS G and an ATL∗sc formula φ, determine whether there exists a norm Nk+1 such that G ⊕Nk+1 |=∅ φ.

In [Alechina et al., 2022], it was shown that the norm synthesis problem for ATL∗ objectives is decidable in (h + 2)- EXPTIME where h is defined before Theorem 1.

3 Cost of Prohibiting Actions

Alechina et al. do not consider the cost of the synthesized norm. In this section, we define the cost of prohibiting actions to agents which we use below to define minimum cost norms. Our approach is general, in the sense that it admits any assignment of costs to prohibiting sets of actions, and can express both the loss of welfare or utility to the agents and/or the cost of enforcing the norm to the normative organisation. However we only consider static costs, and defer consideration of dynamic costs to future work.

First we introduce the notion of a cost of prohibiting an agent to execute a particular action:

The simplest cost function would be to assign the same cost of 1 to each pair of an action and an agent. However, some actions may be more 'expensive' to prohibit or some agents may suffer greater loss of utility from prohibiting the action. For example, a cost of (a, j) may depend on whether j ∈ A for some group of agents A.

Example 2. In the Example 1 scenario, assume that it is significantly more costly to prevent agent 1 from moving; e.g., if agent 1 is an ambulance. Then we could set cost(go, 1) = 100 and cost(go, 2) = 1.

A cost function over pairs (a, j) of actions and agents can be lifted to a cost function over sets of action, agent pairs as:

Depending on the application, for X ∈ 2Ac×Ag , different lifted cost functions may be appropriate.

Example 3. If cost(a, j) is 1 for all actions a and agents j, a natural measure of cost is to sum up the costs of prohibited actions across all agents: cost(X) = ∑(a,j)∈X cost(a, j)

Example 4. If we aim to avoid all costs falling on only a small number of agents, a more natural measure of cost may be to sum the cost of prohibited actions for each agent: cost(X) = maxa∈Ac (∑(a,j)∈X cost(a, j)).

Example 5. Prohibitions such as quarantine restrictions that apply to large numbers of agents may be compared based on the most costly prohibited action, regardless of the identity or number of agents: cost(X) = max(a,j)∈X({cost(a, j)}).

So far, we have considered the costs of prohibiting actions and sets of actions. However, in a run of the system, a norm specifies a sequence of prohibited sets of of actions for each agent. In what follows, we consider two natural interpretations of the cost of a norm, the maximum cost incurred on a run, and the average cost incurred on a run.

4 Maximum Single Step Cost Optimization

The maximum cost of any step along a run is a good measure of the prohibitiveness of a norm; for example, it represents the maximum loss of utility or cost of enforcement incurred due the norm.

Definition 3 (Maximum Single Step Cost). Let cost : 2Ac×Ag -→ N be given. The per step cost of a norm N =⟨Nrm, q0, 2AP, 2Ac×Ag , η, illegal⟩ is

i.e., the cost of the most expensive set of prohibited actions for this norm.

A maximum single step cost least prohibitive norm for a given k-MAS and objective φ is a norm that makes the objective true when added to k-MAS and there is no norm with strictly lower single step cost which makes the objective true. This leads to the following decision problem:

Definition 4 (Maximum Single Step Cost Optimization). Given cost : 2Ac×Ag -→ N, k-MAS and objective φ, is there a norm N of maximum step cost at most m such that N makes φ true when added to the k-MAS.

Example 6. If cost(go, i) = 1 for i ∈ {1, 2} in the Example 1 scenario, the norm in that example is a maximum single step cost least prohibitive norm which ensures the objective

To solve the Maximum Single Step Cost Optimization problem, we reduce it to ATL∗sc model-checking. First we recall the construction of the accessory game given in [Alechina et al., 2022]. The intuition behind this construction is that, given a game G, an extra "normative agent" 0 is introduced who plays a role of a norm (its actions correspond to sets of actions of other agents made illegal by the norm). The resulting game is denoted G ′ .

Construction 1 (Accessory game). For a given game G, the accessory game G ′ = ⟨Ag′ , Ac′ , AP′ , Cap′ , Nrm1, q10 , tr′ , illegal′1 , η′1 ⟩ [Alechina et al., 2022] is defined as:

• Ag′ = {0} ∪ Ag includes a 0-agent, sometimes called the normative agent;
• Ac′ = Ac ∪ (2Ac×Ag ) includes all possible sets of pairs of actions and agents as possible actions;
• AP′ = AP ∪ (Ac × Ag) includes the set of pairs of actions and agents in the atomic propositions;

• tr′ (π′ ,⃗a) = tr(π′↾AP,⃗a-0) ∪⃗a0;
• illegal′ (q1, π′ ) = illegal(q1, π′↾AP);
• η′ (q1, π′ ) = η(q1, π′↾AP).

Formally, the accessory game connects norms in G and strategies for the normative agent 0 in G ′ as follows.

Lemma 1. [Alechina et al., 2022, Lemma 1] For a given 1-MAS G, its accessory game G ′ , and a state π ∈ 2AP, the following two statements hold:

• For every strategy σ0 of agent 0 in G ′ , it holds that outG′ (σ0, (π, q10 ))↾AP = PathsG⊕Nσ0 (π, ⃗q0)↾AP;
• For every normN on G, it holds that PathsG⊕N (π, ⃗q0)↾AP = outG′ (σN , (π, q10 ))↾AP.

The lemma turns the problem of synthesizing a norm for G to satisfy an objective φ into checking for an existence of a strategy for agent 0. The latter can be done by modelchecking G ′ against an ATL∗sc formula ⟨·0·⟩φ. Checking for the existence of a strategy can be done in (h + 1)-EXPTIME for ATL∗sc formulas φ starting with an existential quantifier and (h + 2)-EXPTIME for ATL∗sc formulas starting with a universal quantifier (because ⟨·0·⟩ adds an extra alternation for those formulas).

Using a variant of this construction, we can solve the maximum single step norm optimization problem as follows.

Theorem 2. The Maximum Single Step Norm Optimisation problem can be solved in time (h + 1)-EXPTIME for an existential ATL∗sc formula with quantifier alternation number h, and in (h + 2)-EXPTIME for a universal ATL∗sc formula with quantifier alternation number h.

Proof. Consider the accessory game G ′ defined above and the variant G ′m that differs from G ′ on the capacity function, which is defined for the normative agent 0 as follows:

Clearly, the normative agent in G ′m is allowed to prevent actions only up to cost m at every single iteration.

Therefore, every solution to the normative synthesis in G ′m corresponds to a solution of the single step norm optimization in G, and vice versa.

Another interesting problem related to maximum single step norm optimization consists in finding the optimal cost, that is, the minimum value m∗ for which it is possible to solve the maximum single step norm optimization problem.

Definition 5 (Function Form of Maximum Single Step Optimization). For a given k-MAS G and an ATL∗sc formula φ, find the minimum integer m∗ for which the maximum single step cost optimization problem admits a solution.

If the cost function cost : 2Ac×Ag -→ N is monotone, i.e., A ⊆ B implies that cost(A) ≤ cost(B), by exploiting the solution provided in Theorem 2, we can compute m∗ and the following theorem holds.

Theorem 3 (Optimal Cost Computation). For a given k-MAS G and an ATL∗sc formula φ of quantifier alternation h, computing the optimal cost of the single step norm optimization problem can be solved in time log2(M) · (h+1)-EXPTIME if φ is an existential formula and log2(M) · (h + 2)-EXPTIME if φ is a universal formula, where M = cost(2Ac×Ag ).

Proof. If the cost function is monotone, the maximum cost in G is given when the norm makes all actions for each agent illegal (except noop), which is computed as M = cost(2Ac×Ag ).

We can therefore employ binary search in the range [0,M] where, at each recursive step, with current interval [a, b], we check for the solution of a single step norm optimization with m = a+b 2 . If such a solution exists, we call the binary search over the range [a,m], otherwise, we search over the range [m+ 1, b], and return the value m∗ obtained at the end of the search procedure.

Clearly, the value m∗ is optimal. Regarding the complexity analysis, notice that at each step of the binary search we run a maximum single step norm optimization procedure, which is of complexity (h + 1)-EXPTIME for existential formulas and (h+2)-EXPTIME for universal formulas. As the number of iterations is at most log2(M), the overall complexity is as stated in the theorem.

For non-monotone cost functions, m∗ can be computed by first enumerating costs for all X ⊆ 2Ac×Ag and then solving a single step norm optimization for each of those costs in increasing order.

5 Average Step Cost Optimisation

The maximal single step cost focuses on the greatest restriction imposed by a norm. In many applications, the average degree of restriction is also of interest. In this section, we consider the synthesis of norms that minimize the average cost of the prohibited set of actions over an infinite run.

Example 7. Consider a slightly different scenario to Example 1 where simultaneously executing go only leads to a crash in the initial state of the environment. A norm that makes (go, 2) illegal in the initial state and returns an empty illegal set subsequently ensures the objective in this scenario. Considering the maximal single step cost, this norm is no less prohibitive than the norm from Example 1. However, in the long run (apart from the initial state) the cost of the second norm tends to 0.

We can model such a notion of cost using mean-payoff games. For a sequence r ∈ Rω , the mean-payoff value of r, denoted mp(r) is defined as

We can use the mean-payoff value to define the average step cost of a norm. For a given game G a normNk+1, a legal run r = (π0, ⃗q0), (π1, ⃗q1), . . . in G⊕Nk+1 defines a sequence of costs for Nk+1 defined as

which is a sequence of real numbers on which we can consider the mean-payoff value mp(cost(r)).

Consider a game G, a norm Nk+1, and an ATL∗sc formula of the form ⟨·A·⟩ψ with ψ being a purely temporal formula 1 . Let σA be a strategy profile for the set A of agents such that r |=σA ψ for each r ∈ outG⊕Nk+1 (c0, σA), with c0 being the initial configuration of G ⊕ Nk+1. Note that σA exists if, and only if, G ⊕ Nk+1, c0 |= ⟨⟨A⟩⟩ψ. Denote by Win(G ⊕ Nk+1, ⟨·A·⟩ψ) the set of strategy profiles for A that are a solution (winning) to the model-checking of ⟨·A·⟩ψ against G ⊕Nk+1. Assuming that the set of solution strategy profiles is nonempty, we can define the average step cost of Nk+1 for G and ⟨·A·⟩ψ as follows:

Intuitively, the average step cost of Nk+1 on the formula ⟨·A·⟩ψ depends both on the best behavior of agents in A and the worst behavior of the antagonist agents, i.e., Ag \ A.

Definition 6 (Average Step Cost Optimization). The Average Step Cost Optimization problem amounts to finding a norm Nk+1 such that

for every other norm N ′k+1 , if such a norm exists.

Theorem 4. There exists a game G and an ATL∗sc formula φ for which the Average Step Cost Optimization problem cannot be solved.

Proof sketch. The proof proceeds by considering the game G depicted in Figure 1 and showing two things. The first is that, for every natural number n, there exists a normN n with exactly n internal states such that G ◦ N n |=∅ ⟨·0·⟩GFp with an average step cost of 1n . The second is that there not exist a finite normN such that G◦N |= ⟨·0·⟩GFp whose average step cost is 0. Therefore, it shows an example where the average step cost cannot be optimized.

Theorem ?? states that, in certain cases, we cannot solve the Average Step Cost Optimization problem optimally. By closely analyzing the counterexample in the proof, this is because we can always increase the memory of a given norm and so decrease its mean-payoff cost by, essentially, arbitrarily enlarging the loop on which the periodic costs are applied.

1 Notice that this can also be seen as a ATL∗ formula

However, we can stop adding memory to the norm, as soon as the cost is within ε of the optimal value. We say that a norm Nk+1 is ε-optimal if costmp(Nk+1, ⟨⟨A⟩⟩ψ) ≤ costmp(N ′k+1 , ⟨⟨A⟩⟩ψ) + ε, for every norm N ′k+1 such that G ⊕N ′k+1 |=∅ ⟨·A·⟩ψ.

In the remainder of this section we show that for each ATL∗sc formula of the form ⟨·A·⟩ψ with ψ being a purely temporal formula, we can find an ε-optimal norm that solves the Average Step Cost Optimization problem. In order to do so, we first recall the notion of mean-payoff parity games, introduced in [Chatterjee et al., 2005].

Definition 7 (Mean-Payoff Parity Games). A game graph G = ((V,E), (V0, V1)) consists of a directed graph (V,E) and a partition (V0, V1) of the set V of vertices. All game graphs have the property that every vertex has at least one out-going edge.

A mean-payoff parity game MP = (G, p, c) consists of a game graph G, a priority function p : V → [d] for some d ∈ N and a cost function c : V → R.

In [Chatterjee et al., 2005], it is shown that an optimal strategy for solving a mean-payoff parity game may require infinite memory. However, for each ε > 0 there always exists a finite memory ε-optimal strategy for the maximizing agent [Chatterjee et al., 2005, Lemma 3].

We can use this result to prove the following.

Theorem 5. For every game G, ATL∗sc formula ⟨·A·⟩ψ with ψ being a purely temporal formula, and ε > 0, there exists a ε-optimal normNk+1 such that G ⊕Nk+1 |=∅ ⟨·A·⟩ψ.

Proof sketch. The proof constructs the accessory game as defined in Construction 1 and considers the structural product with the Deterministic Parity Automaton Aψ recognizing all and only the executions that satisfy the LTL formula ψ. This defines a mean-payoff parity game, whose optimal strategy for the maximizer corresponds to the combination of strategies for the normative agent 0 together with those for the agents in coalition A, that is, those that are existentially quantified. Therefore, as shown in [Chatterjee et al., 2005, Lemma 3], we can always find a finite memory ε-optimal strategy for the maximizing agent, which then corresponds to a ε-optimal norm for G over ⟨·A·⟩ψ.

6 RelatedWork

Although there has been a significant amount of work on synthesis with quantitative objectives, e.g. [Gutierrez et al., 2017], there has been much less work on quantitative approaches to norm synthesis.

Previous work on the synthesis of dynamic norms has considered either less expressive objectives, or does not consider costs. [Huang et al., 2016] considers the synthesis of dynamic norms to satisfy Computation Tree Logic (CTL) objectives, and [Perelli, 2019] considers the synthesis of dynamic norms for LTL objectives and Nash equilibria. [Perelli, 2019] addressed LTL objectives and a somewhat different notion of minimality of norms in energy games, where some resource ('energy') required for norm enforcement is periodically replenished. The work closest to our approach is [Alechina et al., 2022] who consider the synthesis of dynamic norms for ATL∗ objectives. Given an ATL∗ objective and a concurrent game structure, a norm is synthesised so that the joint system (with some actions prohibited by the norm) satisfies the objective. However, [Alechina et al., 2022] do not consider the cost of the synthesized norm, and use a less expressive logic as the specification language.

There also exists previous work on generating norms that are not overly restrictive or complex, e.g., [Morales et al., 2015a; Christelis and Rovatsos, 2009]. For example, in [Morales et al., 2015b], a synthesis procedure for state based norms that do not impose unneccessary restrictions on the agents (liberal norms) has been proposed. Issues related to costs have also been addressed in the literature. For example, [Alechina et al., 2013] investigated the problem of whether a given desirable agent behaviour can still take place after a norm is imposed while incurring at most r sanctions (punishments for violating the norm). This can be seen as a cost of the norm. [Cao and Naumov, 2022] considered a logic where 'doing the right thing' (which can be interpreted as complying with a norm) was assigned a cost to the agent (e.g. diving in to save a drowning person clearly has a higher cost than throwing them a lifebuoy).

There exist logics of strategic ability where it is possible to express bounds on costs of agent strategies: RB-ATL [Nguyen et al., 2018] and RB-ATL∗ [Alechina et al., 2018]. However these logics cannot be used to express the bound on the cost of the normative agent's strategy, as, to date, no extensions of these logics with strategy contexts have been proposed. Moreover, RB-ATL and RB-ATL∗ consider the cost of achieving an ATL objective on all infinite runs of the system generated by a strategy. Hence without production of resources by the normative organisation they can express only reachability objectives, and invariant objectives that have a 0 cost on an infinite suffix. In contrast, we make no assumptions about the normative organisation's ability to produce resources, and only consider the cost of the most expensive step on a run and the average cost over an infinite run, which we believe are more appropriate in the context of norm synthesis.

The dynamic norms we consider are effectively implemented in a MAS through regimentation [Grossi et al., 2006]. A regimented norm is impossible to violate due to the design of the MAS. For example, only authorised users can login to the system. An interesting direction for future work is considering the enforcement approach to implementing norms, which imposes a sanction on an agent when a norm is violated, e.g., a fine or social disapproval [Grossi et al., 2006].

7 Conclusions

We presented a formal approach to synthesis of minimal cost dynamic norms to ATL∗sc objectives. We showed that synthesis of minimum cost dynamic norms satisfying ATL∗sc objectives is possible when considering the maximum single step cost, and does not result in increased complexity compared to synthesis of arbitrary norms. We also showed that for nonnested ATL∗sc objectives, it is possible to synthesize ϵ-optimal norms w.r.t. to the average step cost. In future work, we plan to explore tradeoffs between the system-level objective and the cost of the norm.

Acknowledgments

Giuseppe Perelli received funding support from the PNRR MUR project PE0000013-FAIR, the PRIN 2020 projects PINPOINT and Sapienza University of Rome under the "Progetti Grandi di Ateneo" programme, grant RG123188B3F7414A (ASGARD - Autonomous and SelfGoverning Agent-Based Rule Design).