Verifying Normative Behaviour via Normative Mechanism Design

1 Introduction

The overall objectives of multi-agent systems can be ensured by coordinating the behaviors of individual agents and their interactions. Existing approaches advocate the use of exogenous normative environments and organisational models to regulate the agents' behaviors and interactions [5; 6; 7; 11]. Norm-based environments regulate the behavior of individual agents in terms of norms being enforced by means of regimentation or sanctioning mechanisms [5; 6]. Generally speaking, the social and normative perspective is conceived as a way to make the development and maintenance of multi-agent systems easier to manage.

This paper aims at providing a formal analysis of rulebased normative environments from the mechanism design

system is modelled as a concurrent game structure (which is also considered as mechanism) where possible paths in the game structure denote possible execution traces of the corresponding multi-agent environment. Adding norms to the environment may change its set of possible execution traces which in turn correspond to the set of paths of an update of the concurrent game structure. The correspondence between (normative) multi-agent environment and (updated) game structure is an attempt to bridge the gap between normative environments and mechanism design. This relation

Mehdi Dastani

Intelligent Systems Group, Utrecht University, The Netherlands

mehdi@cs.uu.nl

sets the stage for studying formal properties of normative environments such as whether a set of norms implements specific choice functions in specific equilibria. This also allows, for example, to analyse whether groups of agents are willing to obey the rules specified by a normative system. The formal analysis is closely related to work presented in [1; 16] where norms are modelled by the deactivation of transitions. Adding norms to environments in our model may, however, either deactivate transitions or on the contrary add new transitions. Our work is also motivated by [14; 15] where social laws were proposed to be used in computer science to control agents' behaviours.

This paper is motivated by 2OPL (Organisation Oriented Programming Language), which is a rule-based language to implement normative environments in terms of norms and sanctions [5; 6]. In particular, it provides constructs to specify 1) the (initial) state of an environment, 2) the outcomes of agents' actions, and 3) norms and sanctions. The execution of a normative environment specification, with a sequence of agents' synchronized actions as input, determines the normative outcomes of the action sequence. Although many other, even more expressive, languages have been proposed to specify normative environments, 2OPL has the advantage that it comes with a full operational semantics and computationally attractive complexity. This allows normative environments to be studied and analysed as formal mechanisms.

The structure of this paper is as follows. First, we explain our notion of normative environment for multi-agent systems. We propose a formal setting for multi-agent environments and show how they can be related to concurrent game structures and mechanism design. Then, we introduce a specification language for normative multi-agent environments and extend the formal setting of environments with norms and sanctions. Finally, we study and analyse formal properties of normative multi-agent environments using their corresponding concurrent game structure and concepts from mechanism design. We prove the complexity of two verification problems.

2 Formal Framework

2.1 Motivation: Multi-Agent Systems

A multi-agent system consists of a set of agents and an environment in which the agents perform their actions. We assume that agents may or may not be aware of the environment specification, perform only synchronous actions in the environment, and that the outcome of agents' synchronized actions is determined by the environment. In this setting, an environment is specified in terms of an initial state and a set of synchronized action specifications. Agents can change the state of the environment by performing synchronized actions.

Following [5; 6], a normative environment is specified in terms of an initial state, a set of synchronized action specifications, and two sets of rules that represent norms and sanctions. A normative environment determines the outcome of actions by means of action specifications together with norms and sanctions. Norms are represented by counts-as rules [10]. A counts-as rule indicates that a specific state (satisfying the rule's antecedent) counts as a violated state (represented by a specific violation proposition). For example, a traffic norm can be represented by the counts-as rule {carParked, ¬Pay} ⇒ {violPark} stating that parking the car without paying (carParked and ¬Pay) counts as a parking violation (violPark). Sanctions are also represented by rules [5]. A sanction rule connects violation propositions (the rule's antecedent) to state propositions (the rule's consequent). The state propositions in sanction rules denote sanctions and specify how a violated environment state should be repaired and turned back to an optimal state. For example, a sanction rule {violPark} ⇒ {f ine50} connects the parking violation to a state proposition denoting a fine of 50 euro being issued. A pair consisting of a set of counts-as rules and a set of sanction rules is called a norm set.

A normative environment is thus an environment together with a norm set. We assume the sets of counts-as and sanctions rules to be finite.

2.2 Notation: Propositions, States, Actions

We assume that Π is a finite and fixed set of propositional symbols. For each X ⊆ Π, we use X- to refer to {¬p | p ∈ X}, Xc = X ∪ (Π \ X)- (closed-world assumption for X), and Xl = X ∪ X- (literals). Given a set X ⊆ Π and a consistent set Y ⊆ Πl we define the update of X by Y as X⊕Y = {p ∈ Π | p ∈ X∪Y and ¬p ̸∈ Y }. Note that X⊕Y consists of all propositional atoms from Y and extends them with atoms from X as long as they are consistent with (the negated atoms from) Y . We assume the reader is familiar with standard propositional inference, e.g. X |=PL ∧ Y means that formula ∧ Y (∧ Y stands for ∧l∈Y l) is a consequence of theory X using the propositional calculus where X, Y ⊆ Πl . A set X ⊆ Πl is said to be consistent iff X ̸|=PL ⊥.

In the following we use Q to denote a set of states. We assume that states are given by propositional facts, that is Q ⊆ P(Π). Note, that |Q| ≤ 2|Π| . We chose this representation due to the following specific notion of action profile specification. We assume that Agt = {1, 2, . . . , k} is a finite, fixed and non-empty set of agents. We typically use i, i1 , i2 . . . as variables for agent names. Each agent i ∈ Agt is assumed to have at its disposal a set of (individual) actions that it can perform in the environment. A (synchronous) action profile consists of an action for each agent i ∈ Agt. The specification of an action profile ⃗α = (α1 , . . . , αk) in an environment, where αi is the individual action of agent i, is given by (P, ⃗α, E) where P, E ⊆ Πl are consistent sets. The precondition P specifies the applicability of action profile ⃗α. Action profile ⃗α is applicable in a state q iff qc |=PL ∧ P. The postcondition E specifies the effect of performing ⃗α in a state, i.e., how a state changes after the action has been performed. Performing ⃗α in state q results in state q ⊕E. Note that ⊕ is a simple update operator that adds/removes propositional atoms to/from states.

2.3 Concurrent Structures and Strategies

In the following we introduce concurrent (game) structures (CGSS) from [2] (modulo minor modifications). They serve as models for our formal analysis of the environment in multiagent systems. An environment in a multi-agent system is assumed to be specified in terms of a set of states, among which an initial state, and a set of (synchronized) action specifications. Informally speaking, a CGS is given by a labelled transition system where transitions are activated by action profiles. In our setting we construct a CGS from a given set Q of states, an initial state qI ∈ Q, and a set ActSpec of action specifications. A CGS represents possible evolutions of an environment as a consequence of agents performing (synchronized) action profiles. Formally, we define the (ActSpec, Q, qI )-generated CGS as the CGS which is obtained by applying all action profiles to the set of states.

Essentially, these models can be seen as mechanisms. They play the same role as their game theoretic counterparts and define the rules and the structure of the game. Henceforth, we will use the terms CGS and mechanism interchangeably.

Definition 1 (Generated CGS, M) Let Π be a set of atomic propositions, ActSpec be a set of action specifications, Q ⊆ P(Π) be a set of states, and qI ∈ Q. The (ActSpec,Q, qI )- generated CGS is given by M = 〈Agt, Q, Act, ˆ d, d, o〉 where

• Agt = {1, . . . , k} is a nonempty finite set of agents (as before).
• Act = {αi | (P, (α1 , . . . , αk), E) ∈ ActSpec, 1 ≤ i ≤ k} is a nonempty finite set of individual actions.
• ˆ d : Q → P(Actk ) is a function that assigns a set of applicable action profiles to each state. ⃗α ∈ ˆ d(q) iff ∃(P, ⃗α, E) ∈ ActSpec : qc |=PL ∧ P and q ⊕E ∈ Q. Hence, an action profile is applicable if its precondition is satisfied and if the resulting state belongs to Q.
• d : Agt × Q → P(Act) is a function that assigns nonempty sets of applicable individual actions to each agent at each state, i.e. d(i, q) = {αi | (α1 , . . . , αk) ∈ ˆ d(q), 1 ≤ i ≤ k}. We write di(q) instead of d(i, q).
• o : Q × Actk → Q is a partial (deterministic) transition function that determines the outcome state of an action profile performed in a state. It is defined on all (q, ⃗α) with ⃗α ∈ ˆ d(q). We have o(q, ⃗α) = q ⊕ E for (P, ⃗α,E). We assume that other action profiles simply fail and cannot be executed.

If clear from context we will simply use M to denote the (ActSpec, Q, qI )-generated CGS. We use XM to refer to element X contained in M, e.g. QM = Q.

Example 1 For a set Π = {start,m1,m2} of propositions, we define the set ActSpec of action profiles as follows: ActSpec = {({start}, (h, h), {¬start}), ({¬start}, (n, n), {start, ¬m1, ¬m2}), ({start}, (h, t), {m1, m2, ¬start}), ({start}, (t, h), {m1, m2, ¬start}), ({start}, (t, t), {m1}, ¬start)}. Figure 1 shows the (ActSpec, {q0 , q1 , q2 , q3}, q0)-generated CGS M0. For convenience, we identify the label of the node with the set of propositions true in it, e.g. q0 = {start}. Agents can execute actions t, h, and n, standing for "show tail", "show head", and "no operation", respectively.

A strategy of agent i is a conditional plan that specifies what i is going to do in each state. In this paper we focus on state-based strategies (due to obvious reasons they are also called memoryless strategies).

Definition 2 (Strategy, valid) A (memoryless) strategy for agent i is a function si : Q → Act such that si(q) ∈ di(q). A collective strategy sA for a group A = {i1 , . . . , il} ⊆ Agt of agents is a tuple (si1 , . . . , sil ) of individual strategies, one per agent in A. For A = Agt we obtain a (complete) strategy profile. Given two collective strategies sA and sB, A∩B = ∅, we write (sA, sB) to denote the collective strategy of A ∪ B.

We say that a complete strategy profile s is valid iff for all q ∈ Q it holds that s(q) ∈ ˆ d(q).

A path λ = q0 q1 q2 . . . is an infinite sequence of states such that there is a transition between each qm, qm+1. We use λ[m] to denote the mth position on path λ (starting from m = 0) and λ[m,∞] to denote the subpath of λ starting from m.

Definition 3 (Outcome) The outcome outM(q, s) of a valid strategy profile s from state q in model M is the (unique) path λ = q0 q1 q2 . . . such that q0 = q and qm = o(qm-1 , s(qm-1)) for each m = 1, 2, . . ..

2.4 Agent's Preferences

In the analysis of multi-agent systems preferences of agents are often of utmost importance. They are the driving force of agents' behaviours. In our considered models, the executions of the environment and thus the corresponding CGS-paths can be seen as the semantics of preferences. Hence, it is a natural consequence to assume that agents prefer some executions over others. We do not directly consider sets of paths to denote preferences (they may not be regular), but rather temporal formulae. They are used to describe sets of paths, namely all those paths which satisfy them. This idea was already followed in [1; 16; 4] where CTL and ATL, respectively, have been used to model agents' preferences.

Here, we use the temporal logic LLTL [13] for modelling preferences of agents. The logic extends propositional logic with operators that allow to express temporal patterns over infinite sequences of states, called paths. The basic temporal operators are U (until), ✷ (always), ✸ (eventually) and © (in the next state). The language LLTL (Π) is given by all formulae generated by the following grammar, where p ∈ Π is a proposition: ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | ϕUϕ | ©ϕ | ✷ϕ | ✸ϕ. Models for this language are defined as ω-sequences (infinite paths) λ over P(Π), i.e. λ ∈ P(Π)ω . We assume the reader is familiar with the semantics of LTL. We note that in our setting we will not make use of the full expressivity of the logic LTL and its accompanied high computational complexity (cf. Def. 9) which matches the computationally attractive properties of the (restricted) language used for norms and sanctions.

3 Normative MechanismDesign

Here we introduce normative mechanism design by considering a mechanism with norms, sanctions and preferences.

3.1 Basic Setting and Definitions

In social choice theory a social choice function assigns outcomes to given profiles of preferences (see e.g. [12]). Various natural requirements are imposed on social choice functions in order to ensure e.g. fairness. Mechanism design is concerned with creating a protocol/a set of rules such that the outcome agrees with a social choice function f provided that agents behave rationally-in some sense-according to their preferences. In game theoretic terms behaving rationally means to act according to some solution concept S (e.g. the concept of Nash equilibria). If such a mechanism exists it is said that it S-implements f.

We define a normative behaviour function as a function that assigns a set of "desired" environment executions (represented by LLTL -formulae) to each preference profile (a sequence of sequences of LLTL -formulae) of the agents. We refer to the outcome as the normative outcome wrt a specific preference profile. In our view, the aim of normative mechanism design is to come up with a normative mechanism (i.e., an environment specified in terms of actions, norms and sanctions) such that the agents-again following some rationality criterion according to their preferences-behave in such a way that the environment executions stay within the normative outcome. The idea is that norms and sanctions will (de)motivate agents performing specific actions.

We begin with introducing the set of preferences and outcomes defined over elements used in a CGS and in LLTL .

Definition 4 (Preference) A preference list of an agent i ∈ Agt is given by a finite sequence γi = ((ϕ1 , u1), . . . , (ϕl-1 , ul-1), (ϕl, ul)) where each ϕj ∈ LLTL (Π), each uj ∈ N0 for j = 1, . . . , l - 1, ϕl = ⊤, and ul = 0. Intuitively, a path λ is assigned utility uj if ϕj is the first formula in the list which is satisfied on λ.

A preference (profile) is given by ⃗γ = (γ1 , . . . , γk) containing a preference list for each agent. We typically use Prefs to denote a non-empty set of such preferences.

The definition of a normative behaviour function is straightforward given the explanation above.

Definition 5 (Normative behaviour function)

A (M,Prefs)-based normative behaviour function f is a mapping f : Prefs → LLTL (Π).

We have argued above that a normative mechanism may be considered as an environment together with a set of norms and sanctions that guide agents' behaviours in certain directions. Agents are assumed to behave according to their preferences. As the fulfilment of these preferences does only depend on the valuation of states on a path, agents' behavior may be effected if imposing norms and sanctions would cause a modification of states' valuations.

In this paper, we follow [5] and represent norms as a set of counts-as rules and sanctions as a set of sanction rules. The advantages of this approach are the existence of an operational semantics (already implemented), its simplicity (rule based representation and computational complexity), and its expressiveness (p counts-as a violation can be interpreted as it is obligatory that ¬p or p is forbidden). A counts-as rule indicates that a state satisfying its antecedent counts as a state with a specific violation. An example is given in Section 2.1.

Definition 6 (Norm Set M, Rcr , Rsr ) A norm set M over propositions Π is given by M = (Viol,Rcr ,Rsr ) where Viol is a set of propositions disjoint with Π indicating norm violations, Rcr ⊆ P(Πl ∪ Viol) × P(Viol) is a set of count-as rules, and Rsr ⊆ P(Viol) × P(Πl ) a set of sanction rules. For a rule r = B × H ∈ Rcr ∪ Rsr we also write B ⇒ H and use body(r) (resp. head(r)) to refer to B (resp. H). The empty norm set is defined as Mϵ = (∅, ∅, ∅).

The basic idea is that these norms imposed on a model change the states' valuation. The set of counts-as rules applicable wrt a set of propositions X ⊆ Π is defined as follows:

Next, we use function clRcr X (Y ) = {head(r) | r ∈ Appcr (X ∪ Y, Rcr )} and define clRcr X ↑ω as the smallest fixed-point of clRcr X (·), which exists due to Knaster/Tarski's fixed point theorem. This fixed point provides the set of heads of all applicable counts-as rules, i.e. the set of all violation propositions wrt to a set of propositions X. Finally, we define the result of applying the norm set M to a state q ∈ Q as follows:

The resulting state is a state in which all violations are detected and corresponding sanctions are imposed. Note that imposing sanctions modifies the state. Consequently, we define the result of applying the norm set M to a set of states Q as follows: Q ↾ M = {q ↾ M | q ∈ Q}.

That is, we take each state q ∈ Q, determine all applicable count-as rules to q (until a fixed point is reached) and generate the violation propositions, derive the sanctions, and update q with the derived sanctions.

Definition 7 (M ↾ M, normative mechanism ) Let M be the (ActSpec, Q, qI )-generated CGS. The normative update of M with the norm set M, denoted M ↾ M, is defined as the (ActSpec,Q ↾ M, qI ↾ M )-generated CGS. We call the tuple (M,M ) a normative mechanism.

We would like to point out that M ↾ M is a mechanism whereas (M,M ) is a normative mechanism.

Note that after a normative update took place some action specifications may become inapplicable where others become applicable, so we remove and create transitions which is an important difference to [1].

3.2 Implementation of Normative Mechanisms

This section examines the question of whether specific outcomes of a normative mechanism agree with a normative behaviour function. In this setting it is assumed that agents behave rationally in some way (they follow some solution concept). In order to use these game theoretic concepts we link our setting to strategic games.

Definition 8 (CGS ❀ strategic game) Let M be a CGS, k = |AgtM|, ⃗γ = (γ1 , . . . , γk) ∈ Prefs be a preference profile, and qI be the initial state inM.

We define Γ(M, ⃗γ, qI ), the strategic game associated with M, ⃗γ, as the strategic game 〈AgtM, Σ1 , . . . , Σk, μ〉 (cf. [12]) where AgtM is the set of players, Σi is the set of strategies of player i, and the payoff function μ = (μ1 , . . . , μk) is defined as follows:

where 1 ≤ i ≤ k, γi = ((ϕ1 , u1), . . . , (ϕl-1 , ul-1), (ϕl , ul)) and j is the minimal index such that outM(qI , s) |=LTL ϕj. (We note that μ is well-defined as ϕl ≡ ⊤).

A game theoretical solution concept, e.g. Nash equilibria or dominant strategies, can be considered as a function S whose domain is the set of strategic games and its image is a set of strategy profiles. That is, for each strategic game G = (Agt, (Σi), μ) we have that S(G) ⊆ ×i=1,...,|Agt|Σi.

We assume the reader is familiar with the solution concept of Nash equilibria and dominant strategy equilibria and refer to [12] for more details. We use NE and DOE to refer to these concepts, respectively.

We lift the notion of solution concepts to a CGS M by defining S(M, ⃗γ, q) := S(Γ(M, ⃗γ, q)).

Definition 9 (M S-implements f over M, qI , Prefs)

We say that a norm set M S-implements normative behaviour function f over M, qI ,Prefs iff the following condition is satisfied for all ⃗γ ∈ Prefs and all ∀s ∈ S(M ↾ M, ⃗γ, qI ) : outM↾M(qI , s) |=LTL f (⃗γ ). If there is some M that S-implements f over M, qI ,Prefs, we say that f is S-implementable over M, qI , Prefs.

We highlight that our notion of implementation is given wrt. a norm set and not wrt. a mechanism per se.

Example 2 We consider the CGS M from Example 1 with qI = q0. By strategy sx for x ∈ {t, h} we denote the strategy with sx(q0) = x and sx(q) = n for all other states q ̸= q0. We define Prefs = {γ 1 , γ 2 } with γ 1 = (((✸(m1 ∧ m2), 1), (⊤, 0)), ((✸m2, 1), (⊤, 0))) and γ 2 = (((✷¬m1, 1), (⊤, 0)), (✸(m1 ∨ m2 ∧ ✷¬(m1 ∧ m2, 1), (⊤, 0)))). Let the following normative behaviour function f be given: f (γ i ) = ✷¬(m1 ∧ m2) for i ∈ {1, 2}. First of all we note that the (empty) norm set M∅ does not NE-implement f over M, q0 ,Prefs because NE(M, γ 1 , q0) = {(st, sh), (sh, st)} but f (γ 1 ) is false on both paths resulting from these profiles. (We recall that M ↾ M∅ = M.)

Now, consider the norm set M = ({v}, {{¬start,m1,m2} ⇒ {v}}, {v} ⇒ {¬m1}}}). The mechanism M ↾ M is similar to M but state q2 = {m2}. In particular, both action profiles (h, t) and (t, h) are not applicable anymore. Then, M NE-implements f over M, q0 , Prefs. In Figure 2 we have shown the strategic games Γ(M, γ i , q0) and Γ(M ↾ M, γ i , q0) for i = 1, 2. The Nash equilibria in each game are highlighted in bold letters. In the game Γ(M ↾ M, γ 2 , q0) we have that NE(M ↾ M, γ 2 , q0) = {(sh, sh), (st, st)}, outM↾M(q, (sh, sh)) = {(q0 q1)ω }, and outM↾M (q, (st, st)) = {(q0 q3)ω }. For each path λ in the outcome we have λ |=LTL f (γ 1 ). The same holds for γ 2 .

4 Verification and Complexity Issues

In this section we consider the complexity of the problem whether some norm set implements some normative behavior function and the complexity needed to determine whether such a norm set exists at all. In this paper we focus on Nash equilibrium implementability. These results are important in order to check whether a normative environment ensures desired behaviors or whether some norm set can be constructed to enforce such behaviors. Due to space limitations we can only present the basic setting and the main results.

Encoding. How do we measure the input? Often, the number of action specification/transitions is exponential in the number of states but could be expressed in a more compact form. A compact action specification is given by (P, ξ, e) where P is the precondition defined as before, ξ indicates which actions are applicable (explained below), and e is a list ((ξ1 , S1), . . . , (ξh, Sh)) where each Sk ⊆ Πl is consistent, 1 ≤ k ≤ h. Each formula ψ ∈ {ξ, ξ1 , . . . ξh} is a Boolean formula over propositions execiα where i ∈ Agt and α ∈ Act. We require that |=PL ξ (⃗α) → ξk(⃗α) for some k where ⃗α = (α1 , . . . , αk) is an action profile and ψ(⃗α) is used to refer to the Boolean formula over {⊤,⊥} obtained by replacing each execiα with ⊤ (resp. ⊥) if αi = α (resp. αi ̸= α). The semantics of e is defined as [[e(⃗α)]] := Sj where j, 1 ≤ j ≤ h, is the minimal index such that |=PL ξj(⃗α). Therefore, (P, ξ, e) gives rise to (several) action specifications (P, ⃗α, [[e(⃗α)]]) if |=PL ξ (⃗α). We use ˆ ActSpec to denote the set of compact action specifications and ActSpec to refer to its associated set of (non-compact) action specifications.

Problems. In this chapter we consider the (S,M )- implementation problem IPSM which is given by all P = (Π,Q, ˆ ActSpec, qI , f, Prefs , M ) such that the norm set M S-implements f over M, qI ,Prefs. (Recall, that M is the (ActSpec,Q, qI )-generated CGS.) The S-implementation problem IPS contains all P ′ = (Π,Q, ˆ ActSpec, qI , f, Prefs) such that there is a norm set M with (Π,Q, ˆ ActSpec, qI , f, Prefs , M ) ∈ IPSM . We assume that f is computable in polynomial deterministic time wrt. the size of the input. The size of Q and Π is defined as the number of their elements. The size of a compact action specification is |(P, ξ, e)| = |P| + |ϕ| + ∑hi=1 |ξi| + |Si|. Prefs and M are measured in the canonic way.

The following result holds due to the restricted syntax of the language used to define norm sets: fixed points can be calculated in polynomial deterministic time.

Proposition 1 Given ˆ ActSpec, Q, and qI , we can compute Q ↾ M, and qI ↾ M in polynomial deterministic time.

Theorem 2 The problem IPNE M is ΠP2 -complete.

Proof. [Idea] Hardness is shown by a reduction of 2QBF, a well known ΣP2 -complete problem [8], to the complement of IPNE M . In [3] it is shown that a 2QBF-formula φ ≡ ∃x1 , . . . , xm∀xm+1 , . . . , xnϕ(x1 , . . . , xn) is true iff a player v (the verifier, controlling variables x1 , . . . , xm) has a winning strategy sv (fixing a valuation for variables x1 . . . xm) against each strategy sr (fixing a valuation for variables xm+1 . . . xn) of the refuter r (controlling variables xm, . . . , xn) to ensure some LTL-formula (in [3] ATL is used but it can also be formulated in terms of LTL).

The new part in our proof is to construct a preference list, a normative behaviour function, and a normative mechanism such that a "witnessing" strategy sv of v (see above) exists iff there is a Nash equilibrium which falsifies f given the other ingredients (this is exactly the complement of NEimplementability). Our proof is also motivated by [9].

Membership is shown by guessing a strategy profile s = (s1 , . . . , sk) and checking whether any agent i can improve its outcome by deviating from si (again, si is nondeterministically guessed). If this is not the case s is a Nash equilibrium and all other steps can be done in polynomial deterministic time. This shows that the complement of IPNE M can be solved in ΣP2 . ■

Proof. [Idea] In order to prove this result we extend the idea from Theorem 2. We reduce a complemented 3QBF formula φ ≡ ∀y1 , . . . , yl∃x1 , . . . , xm∀xm+1 , . . . , xnϕ(y1 , . . . , yl, x1 , . . . , xn) (this problem is well known to be ΠP3 - complete [8]) to the complement of an IPNE instance. The idea is to use a norm set to generate truth valuations of the universally quantified variables y1 , . . . , yl. Once a norm set is fixed we apply the reduction from Theorem 2. ■

5 Conclusions and Future Research

In this paper we have proposed normative mechanism design as a formal tool for analysing normative environment programs such as 2OPL programs. We have shown how to abstract from a particular environment specification language and how to apply methods from mechanism design to verify whether some norm restrictions imposed on a multiagent environment agree with the behaviour the designer expects. More precisely, we have introduced normative behaviour functions for representing the "ideal" behaviour of multi-agent environments with respect to different sets of agents' preferences. The latter has enabled us to apply concepts from game theory to identify agents' rational behaviour. These formal ideas can now be used to verify whether a norm set (a set of norms and sanctions) is sufficient to motivate agents to act in such a way that the behaviour described by the normative behaviour function is met.

We have defined a norm set in such a way that is can modify facts in the environment states (cf. Def. 6 and 7). As the language used for modelling agents' preferences and the facts in norm sets are based on the same set of propositional symbols, a normative mechanism can steer the behaviour of each agent in (almost) arbitrary ways. This notion of mechanism is very powerful. A first refinement would be to identify a subset ΠM ⊆ Π of facts and assume that a norm set can only modify state valuations with respect to this set. Such a mechanism can be much weaker but also more natural.

Another direction of future research is to consider robustness against group deviation. Our approach can be extended such that each agent a has its "own" set Πa of propositional symbols which is used for its preference formulae. If we now want that some agents are not sensitive to norms and sanctions we simply define the set ΠNF of facts that are used in a norm set such that ΠNF ∩ Πa = ∅. Another alternative is to take on a more game theoretical point of view in the line with [1; 4]. For example, one may consider partial strategies which assume that only subgroups of agents play rationally. Then, the outcome is usually not a single path any more, but rather a set of paths. This gives rise to a notion of (S,A)- implementability.

We have investigated the problem, given M as a (ActSpec, Q, qI )-generated CGS, a set of agents' preferences Prefs, and a normative behaviour function f, whether there is a norm set M which S-implements f over M, qI and Prefs. In future work it would be interesting to find settings in which such norm sets can be constructed efficiently, i.e. "implementing" some norms and sanctions. We also plan to extend our analysis to other implementability notions apart from Nash equilibria, e.g. dominant strategy equilibrium implementability.

Again, we like to emphasize that our work is closely related to [1; 16]. In the former, labelled Kripke structures are considered as models supposing that each agent controls some transitions. A norm is then considered as the deactivation of specific transitions. The main difference to our work is that the outcome is assumed to be independent of the preferences where we consider a more general setting captured in terms of normative behaviour functions. Also, norms in our approach can either deactivate or create a transition. It is also important to recall that our focus is of a more practical nature. We try to implement and to analyse mechanisms from a practical point of view, i.e., how to specify normative multi-agent environments. This is best indicated in the way we construct CGSS: They are generated from action specifications.