Computational Disaster Management

1 Introduction

Norms have been widely proposed as a means of coordinating and regulating the behaviours of agents within a multiagent system (MAS). Norms can be viewed as standards of behaviour which specify that certain states or sequences of actions in a multi-agent environment are prohibited or incur some sanction. For example, the designer of an electronic marketplace may want to encourage registration before exchanging goods and timely payment for goods sold. Norms can be implemented in a MAS environment through norm enforcement or norm regimentation. Enforcement imposes sanctions on bad states or behaviours, whereas regimentation eliminates bad states and behaviours.

Norms can be implemented directly as constraints on actions (or action sequences) within a MAS environment. However, there are a number of reasons to separate the implementation of the environment as a set of (physical) behaviours from the implementation of norms that control and coordinate agents' behaviours. One reason is that normative aspects of an environment typically change more frequently than its physical aspects (e.g., possible actions). Another reason for this separation of concerns is to support the development and maintenance of environments in a modular and reusable manner, by making the development and maintenance of norms independent of the development and maintenance of the physical aspects of the environment. Thirdly, enforced (non-regimented) norms are different from the physical constraints on actions typically expressed in action preconditions, as norms can be violated. The violation of en- Brian Logan University of Nottingham Nottingham, UK bsl@cs.nott.ac.uk forced norms incurs sanctions, and the type of sanction applied depends on the circumstances under which norms are violated. Lastly, a separate implementation of norms makes it easier to analyse the effect of updating the same physical environment with different sets of norms. We call the addition of a set of norms to a MAS environment a normative update of the environment.

A key problem in the design of normative MAS is whether a proposed normative update will have the effect intended by the designer of the system. Previous work on verifying properties of normative updates has considered only a relatively simple view of norms where some actions or states are designated as violations.

In this paper, we focus on conditional norms with deadlines and sanctions [Tinnemeier et al., 2009], and present a formal framework that allows us to reason about the effects of a normative update of a MAS environment by a set of conditional norms. Conditional norms are triggered (detached) in certain states of the environment and have a temporal dimension specified by a deadline. The satisfaction or violation of a detached norm depends on whether the behaviour of the agent(s) brings about a specified state of the environment before a state in which the deadline condition is true. Norms can be enforced by means of sanctions or they can be regimented by disabling actions in specific states. We introduce two new logics to reason about conditional norms, CTLS (CTL with Sanctions) and ATLS (ATL with Sanctions), which allow us to express properties such as 'the agent(s) are unable to bring about a state satisfying φ' and 'the agent(s) are unable to bring about a state satisfying φ without incurring at least sanctions Z'. Sanction and regimentation properties are verified by means of model checking. We prove that the complexity of model-checking problems for CTLS and ATLS is PSPACE.

2 Normative Update

Let Π be a finite set of propositional variables. Π is partitioned into a set of physical atoms Πb and a set of sanction atoms Πs. The distinguished atom san⊥ ∈ Πs denotes the sanction in regimented norms (that is, norms which cannot be violated by agents).

Definition 1 (Physical Transition System) A physical transition system is a tuple M = (S, R, V ), where S is a finite, non-empty set of states, R ⊆ S × S is a transition relation, and V is a propositional valuation S -→ 2Π.

Intuitively, M describes the computational behaviour of a (multi) agent system. R corresponds to agents executing actions, and actions have preconditions and effects specified in terms of physical atoms that are satisfied by the transitions.

Before we can define norms and normative update, we need some temporal logic preliminaries. Given a physical transition system M = (S, R, V ), a path through M is a sequence s0, s1, s3, . . . of states such that siRsi+1 for i = 0, 1, . . .. A fullpath is a maximal path and a run of M is a fullpath which starts from a state sI ∈ S designated as the initial state of M. We denote fullpaths by ρ, ρ′ , . . . , and the state at position i on ρ by ρ[i]. For a state s ∈ S, the tree rooted at s is the infinite tree T(s), obtained by unfolding M from s (the nodes of T are finite paths starting from s ordered by the prefix relation). T(M) = T(sI) is the computation tree of M. Note that branches of T(M) are runs of M.

To make the notions of norm violation, enforcement and update precise, we use Computational Tree Logic with Past (CTL∗ +Past), see, e.g., [Schnoebelen, 2003]. The syntax of CTL∗ +Past formulas is defined as follows:

where X means next state, X -1 means previous state, U stands for until, S for since, and E for 'exists a run'. The truth definition for formulas is given relative to T(M), a run ρ and the state at position i on ρ:

T(M), ρ, i |= ¬φ iff T(M), ρ, i ̸|= φ

• T(M), ρ, i |= φUψ iff ∃j ≥ i such that T(M), ρ, j |= ψ and ∀k : i ≤ k < j, T(M), ρ, k |= φ

• T(M), ρ, i |= φS ψ iff ∃j ≤ i such that T(M), ρ, j |= ψ and ∀k : i ≥ k > j, T(M), ρ, sk |= φ

T(M), ρ, i |= Eφ iff for some run ρ′ which is identical to ρ on the first i indices, T(M), ρ′ , i |= φ.

Fφ (some time in the future) is defined as ⊤Uφ, Gφ (always in the future) is defined as ¬F¬φ.

Definition 2 (Norms) Let cond, φ, d be boolean combinations of propositional variables from Πb and san ∈ Πs. A conditional obligation is represented by a tuple (cond,O(φ), d, san) and a conditional prohibition is represented by a tuple (cond, P (φ), d, san). A norm set N is a set of conditional obligations and conditional prohibitions.

Conditional norms are evaluated on runs of the physical transition system. A conditional norm n = (cond, Y (φ), s, san), where Y is O or P, is detached in a state satisfying its condition cond. Detached norms persist as long as they are not obeyed or violated, even if the triggering condition of the corresponding conditional norm does not hold any longer. A detached obligation (cond,O(φ), d, san) is obeyed if no state satisfying d is encountered before execution reaches a state satisfying φ, and violated if a state satisfying d is encountered before execution reaches a state satisfying φ. Conversely, a detached prohibition (cond, P(φ), d, san) is obeyed if no state satisfying φ is encountered before execution reaches a state satisfying d, and violated if a state satisfying φ is encountered before execution reaches a state satisfying d. If a detached norm is violated in a state s, the sanction corresponding to the norm is applied (becomes true) in s. We say a detached norm is annulled in a state s′ immediately after a state s in which the norm is obeyed or violated, unless the same norm is detached again in s′ . Note that given an original physical transition system, we cannot say whether a norm is violated in a given state s; to determine that, we need to know the path taken to reach s (e.g., whether any norms were detached in the past), and there may be more than one path to s. This is the reason why conditional norms are evaluated on runs of the system.

Definition 3 (Norm Violation) A state ρ[i] violates a conditional obligation (cond, O(φ), d, san) on run ρ in T (M) iff

ρ[i] violates a conditional prohibition (cond,P(φ),d,san) iff

We distinguish two kinds of sanctions: regimentation sanctions and resource sanctions. Regimentation sanctions arise in the context of wholly or partially regimented normative systems, where the normative system enforces norms to ensure that certain behaviours never occur. If a norm labels a state with the distinguished sanction atom san⊥, then the run containing this state is removed from the set of runs of the system by the normative update. Resource sanctions, on the other hand, arise in the context of (wholly or partially) unregimented normative systems, which treat sanctions essentially like fines or taxes. Such sanctions penalize rather than eliminate certain execution paths by reducing the resources of the agent. An undesirable state (from the point of view of the system designer) may or may not be achievable by an agent (or agents) depending on the resources the agent is able or willing to commit to achieving it.

The normative update of a physical transition system is defined by applying sanctions to violating states in the execution paths of the system, and removing regimented paths.

Definition 4 (NormEnforcement) Let N be a norm set, and n = (cond, Y (φ), d, san) ∈ N be a norm (for Y ∈ {O, P}). The norm n is enforced on a run ρ when, for every i, ρ[i] violates n iff ρ, i |= san. The norm set N is enforced on ρ iff all norms in n ∈ N are enforced on ρ.

Given a physical transition system M and a set of norms N, a normative update of M with N, denoted by M N , is realized by updating the tree T(M) of M with the norm set N.

Definition 5 (Normative Update) Let M = (S, R, V ) be a finite physical transition system with initial state sI and N a finite set of conditional obligations and prohibitions. A normative update of M with N, M N , is T(M) where all norms from N are enforced on all runs. In other words, in each tree node s′ , V N (s′ ) contains sanction atoms for all norms violated in s′ . Paths which contain a state satisfying the distinguished sanction atom san⊥ are removed from M N .

We assume that M N is non-empty, i.e., that regimentation does not remove all possible paths from the system (cf the 'reasonableness assumption' in [ ˚Agotnes et al., 2010]).

3 CTLS

We now show how to reason about the effects of updating a physical transition system with norms. To simplify the presentation, in this section we first consider the case of a single agent, and consider the multi-agent case in Section 4. We use an extension of Computational Tree Logic CTL [Clarke et al., 1986] with sanction bounds which we call CTLS .

To express properties of a normative update, we need to be able to talk about the number of sanctions applied on a run. For simplicity, we assume that each norm i has its own distinct sanction proposition sani, apart from regimented norms which all have san⊥ as the sanction atom. To say that a path contains no occurrences of san0, at most 2 occurrences of san1, and at most infinitely many occurrences of san2 we will use sanction bound expressions which are multisets of the form {san1, san1, ∞ ∗ san2}. We will use abbreviations 0 for the multiset which contains 0 occurrences of any sanctions, and ∞ for the multiset where the multiplicity of each sanction is ∞. Below, we use set notation for multisets with the obvious semantics. In particular, the union of two multisets Z1 and Z2 is a multiset, where the multiplicity of each element is the sum of its multiplicities in Z1 and Z2, and n + ∞ = ∞ for any multiplicity n. We also use ≤ to compare two multisets, again as an obvious generalisation of set inclusion (Z1 ≤ Z2 iff the multiplicity of each element in Z1 is less then or equal to its multiplicity in Z2, with n ≤ ∞ for any multiplicity n).

The language of CTLS is defined by:

where Z is a multiset of sanction atoms (sanction bound). E≤Z means 'there exists a path of sanction cost at most Z'. We define E≤Z Fφ =df E≤Z ⊤Uφ. Note that CTL operators are a special case of CTLS operators with an infinite bound for all sanctions.

We use the abbreviation sanctions(s) for a state s ∈ S to mean the set of sanction atoms in V (s). (Recall that, in a tree, each s is on a unique run.) For a run ρ, sanctions(ρ) = ∪isanctions(ρ[i]) is a multiset of sanction atoms.

The truth of CTLS formulas is defined relative to a tree model T (intuitively, a normative update) and a state in T :

• T, s |= E≤Z Xφ iff there a fullpath ρ′ with ρ′ [0] = s, such that T, ρ′ [1] |= φ and sanctions(ρ′ ) ≤ Z
• T, s |= E≤Z φUψ iff there exists a fullpath ρ′ with ρ′ [0] = s, such that for some n ≥ 0, T, ρ′ [n] |= ψ and for every i, i < n, T, ρ′ [i] |= φ and sanctions(ρ′ ) ≤ Z
• T, s |= E≤Z Gφ iff there exists a fullpath ρ′ with ρ′ [0] = s, such that for every i, T, ρ′ [i] |= φ and sanctions(ρ′ ) ≤ Z.

In general, two kinds of properties of a normative update are of interest: liveness properties and safety properties. Liveness properties check that, following a normative update, desirable states (from the point of view of the system designer) are still possible and can be achieved without an agent incurring sanctions, or with some 'admissible' number of sanctions. For example, if φ is a desirable state, then E≤0F φ is a liveness property which says that there is an execution path which achieves φ and no state of this path has a sanction applied. Conversely, safety properties check that it is impossible for an agent to reach states where some undesirable property holds without incurring some minimum level of sanctions. For example, if ψ is an undesirable property, then the formula ¬E≤sanFψ says that there is no execution path where ψ is reachable and the set of sanctions is less than san. So the agent may be able to achieve ψ, but it will have to pay more than san.

Model-Checking

The model-checking problem for a normative update of a single agent physical transition system takes as inputs a physical transition system M = (S, R, V ) with initial state sI ∈ S, a finite set of conditional norms N, and a formula φ of CTLS . It returns true if M N , sI |= φ, and false otherwise.

Theorem 1 The model-checking problem for a normative update of a single agent physical transition system is in PSPACE.

Proof. We give a non-deterministic algorithm for checking whether for an arbitrary s, M N , s |= φ, which requires space polynomial in |S|, |N| and |φ|. This shows that the model-checking problem is in NPSPACE. Since NPSPACE=PSPACE, it is also in PSPACE.

The algorithm is as follows. Assume we have a set of subformulas of φ closed under single negations, ordered in increasing order of complexity. We label states with subformulas in φ in order. For subformulas which do not start with a path quantifier, the algorithm is as for propositional logic (constant time), and for subformulas which start with a path quantifier with an infinite bound, the algorithm is as for CTL. If we have a subformula of the form E≤Z ψ, then we guess a run ρ which goes through s, and continues infinitely (note that such a run can still be represented using space polynomial in |S|) such that the part of ρ starting in s satisfies ψ, accumulates no more than Z sanctions, and does not violate any norms which result in the sanction san⊥. Note that to check the number of sanctions incurred in the future of s, we need to knowwhat happens on the run before s. □

Theorem 2 The model-checking problem for a normative update of a single agent physical transition system is PSPACE-hard.

Proof. The proof is by reduction of the QSAT (Satisfiability of Quantified Boolean Formulas) problem (which is a PSPACE-complete problem) to the model-checking problem for a normative update. The idea of the proof comes from the PSPACE-completeness proof for ATL+ with perfect recall in [Bulling and Jamroga, 2010].

The QSAT problem takes as an input a formula of the form ∃p1∀p2 . . .Qpnφ where pi are propositional variables, the quantifier for pi is ∃ if i is odd and ∀ if i is even, and φ is a propositional formula in negation normal form (negations only apply to propositional variables).

For each quantified boolean formula ψ = ∃p1∀p2 . . .Qpnφ, we are going to construct a structure Mψ which encodes conditions for its satisfiability: it starts with transitions corresponding to selection of truth values for the variables, continues with a parse tree of φ, then evaluates literals at the leaves of the parse tree and finally transits to a 'success' or 'failure' state. We are also going to introduce a set of norms N which prohibit evaluating pi to true and false simultaneously. Then we reduce the problem of whether ψ is true to the problem of whether an update of Mψ with N satisfies a CTLS formula ψ′ which says that there is a sanction-free way to traverse the structure which ends in the success state. The formula ψ′ is polynomial in the size of ψ, as are Mψ and N.

The structure Mψ and formula ψ′ use the following propositional variables: for each pi in ψ, pi itself and also a special variable notpi (the first one becomes true if pi is assigned the value true, and the second if it is assigned false). We also need a propositional variable yes which holds in the success state.

Mψ consists of three 'sections'. In the first section, for every variable pi in φ, we have a state si from which there are two transitions to states si⊤ and si⊥; in si⊤ pi is true, and in si⊥ notpi is true. From each of these states, there is a transition to si+1. From the last two states in the value selection section, sn⊤ and sn⊥, there is a transition to the first state sφ in the second (parse tree) section. From each state sχ in this section, there are n transitions to the states corresponding to the arguments of the main connective of χ. Unlike the parse tree assumed in [Bulling and Jamroga, 2010], we are building an and-or tree: at one level there are n conjuncts, at the next level m disjuncts, etc. When we start hitting the literals, we add a dummy single transition to the next state to make sure that the and-or tree has the same depth on all branches. The last level of states in the parse tree section are states corresponding to literals pi or ¬pi: spi or s¬pi . The last section of the model is as follows. From a state spi corresponding to a positive literal, there are two transitions to states s′i⊤ and s′i⊥ which satisfy pi and notpi respectively, and there is a transition from s′i⊤ to the syes state which satisfies yes and a transition from s′i⊥ to the sno state. From a state s¬pi corresponding to a negative literal, there are also two transitions to states s′i⊤ and s′i⊥ which satisfy pi and notpi respectively, but this time there is a transition from s′i⊤ to the sno state and a transition from s′i⊥ to the syes state. Both syes and sno have transitions to themselves.

The norms prohibit going through a s′i⊥ state after going through a si⊤ state. This intuitively corresponds to prohibiting assigning first true and then false to pi. Similarly they prohibit going through a s′i⊤ state after going through a si⊥ state. For each pi we have two prohibitions, (pi, P(notpi), yes, san+i ) and (notpi, P(pi), yes, san-i ).

Finally, the formula ψ′ is built as follows. It starts with normal CTL quantifiers (quantifiers of sanction bound infinity) which say that there exists an assignment to p1 such that for all assignments to p2 etc.: EX EX AX EX . . . (the second EX after each quantifier describes the transition from si⊤ or si⊥ to si+1 state). Then it does the same for the and-or tree section of Mψ: for 'and' levels it uses AX, and for 'or' levels it uses EX. Finally it says E≤0Xyes, namely there is a way of making φ true without violating the norms. □

Translation to CTL∗ + P ast

Non-deterministic algorithms are primarily of theoretical interest. Below we give a more concrete algorithm for modelchecking CTLS by reducing the problem to model-checking CTL∗ + Past. It involves a straightforward translation of sanction bounds into CTL∗ + Past formulas which encode information about sanctions. We can then apply a modelchecking algorithm for CTL∗ + P ast.

Before we state the translation, we introduce an expanded representation for sanction bounds. Namely, for a sanction bound Z, the expanded representation e(Z) is of the form n1∗san1, . . . , nm∗sanm where ni is the multiplicity of sani and a sanction for each non-regimented norm in N occurs unless its multiplicity is ∞. In other words, if sani ̸∈ Z, then it occurs in e(Z) with ni = 0, and if san occurs with multiplicity∞, we do not include it in e(Z).

The translation from CTLS to CTL∗ + Past only affects path operators with sanction bounds:

where e(Z) = n1 ∗ san1, . . . , nm ∗ sanm. Each formula φ(ni+i)∗sani is a CTL∗ +Past formula which says that sanction sani is applied ni + 1 times or more; its negation therefore states that sanction sani is applied at most n times. Its precise form depends on whether the corresponding norm is an obligation or a prohibition. φsan⊥ states that some regimented norm has been violated on the run.

On any run, for there to be (at least) ni + 1 violations of a conditional obligation (cond,O(p), d, sani) in the future of a state sj, there should be either at least ni + 1 violations from obligations detached in sj or in future states sk, k > j, or one of the obligations was detached in the past (in a state si, i < j) and the remaining ni violations result from obligations detached in the future. Note that in both cases, all the violations (and hence sanctions) occur in the current state or in future states. The case in which all ni + 1 norms are detached in the current or future states can be expressed as a formula φfuture (ni+1)∗sani where

The case in which one instance of the norm was detached in the past and violated in the future of sj (note that there can be at most one such instance) can be expressed as a formula φpast sani where

and the formula expressing that ni norms are detached in the current and/or future states is just φfuture (ni)∗sani . The complete formula which says that the obligation is violated at most ni times is then:

Similarly for conditional prohibitions, we need to write a formula saying that (cond, P(q), d, sani) is detached and violated at least ni + 1 times in the current and/or future states

where

and a formula which says that it is detached once in the past and violated in the current or a future state:

The complete formula which says that the prohibition violated at most ni times has the same form as for obligations.

Finally, φsan⊥ is defined as a disjunction which says that one of the regimented norms is violated at least once.

If the sanction bound is written as a multiset (i.e., {san1, san1, san2}) the translation above is polynomial in the original formula and in |N|, and CTL∗ + Past modelchecking is PSPACE-complete [Schnoebelen, 2003]. In practice this means that a concrete model-checking algorithm will be exponential in the formula size. For the general case, when several non-regimented norms may have the same sanction atom, the approach above will result in a translation which is in the worst case exponential in the sanction bound. This would result in a double exponential in the formula if CTL∗ +Past model-checking is used. However, translation into CTL∗ + Past is not the only way of defining a concrete model-checking procedure for normative updates. It is possible to give an algorithm for the general problem (i.e., where multiple norms can result in the same sanction atom) that is exponential in the sanction bound, but polynomial in the number of states and edges in M. The algorithm extends a standard CTL algorithm with an additional pass over M to compute a labelling that records all non-dominated sanction bounds on paths from each state. We do not include the algorithm in the paper due to space limitations.

4 ATLS

In this section we consider normative updates of multi-agent systems. We assume that a physical multi-agent system is represented as a concurrent game structure (CGS).

To express properties such as 'a group of agents C cannot maintain property φ unless they incur sanction san at least once' we extend the syntax of Alternating Time Temporal Logic ATL [Alur et al., 2002] with sanction bounds. We call the resulting logic ATLS. The syntax of ATLS is defined relative to a set of propositional variables Π, a finite set of agents A, and a set of sanction atoms Πs ⊆ Π as follows:

where C ⊆ A and Z is a multiset of atoms from Πs. Intuitively, 〈〈C〉〉≤Z γ means 'the group of agents C has a strategy, all executions of which incur at most Z sanctions and satisfy the formula γ, whatever the other agents in A \ C do'.

Definition 6 (Concurrent Game Structure) A Concurrent Game Structure (CGS) is a tuple M = (S, V, a, δ) which is defined relative to a set of agents A = {1, . . . , n} and a set of propositional variables Π, where:

• S is a non-empty set of states
• V : S → ℘(Π) is a function which assigns each state in S a subset of propositional variables
• a : S×A → N is a function which indicates the number of available moves (actions) for each player i ∈ A at a state s ∈ S such that a(s, i) ≥ 1. At each state s ∈ S, we denote the set of joint moves available for all players in A by A(s). That is

• δ : S × N|A| → S is a partial function where δ(s,m) is the next state from s if the players execute the move m ∈ A(s).

In what follows, we assume norms apply to individual agents. The definition of a normative system therefore does not change, except that each norm now has an extra parameter representing the agent to whom the norm applies: a conditional obligation for agent i is represented by the tuple (cond, O(i, φ), d, san) and a conditional prohibition is represented by the tuple (cond, P(i, φ), d, san) where i ∈ A. As before, we assume that each norm has a unique sanction atom. We do not explicitly model group norms: rather we assume that each group obligation and prohibition is decomposed into individual obligations and prohibitions for the agents in the group, and that the sanction associated with the group norm is automatically decomposed into sanctions associated with the individual norms.

Definition 7 (Move) Given a CGS M and a state s ∈ S, a move (or joint action) for a coalition C ⊆ A is a tuple σC = (σi)i∈C such that 1 ≤ σi ≤ a(s, i).

By AC(s) we denote the set of all moves for C at state s. Given a move m ∈ A(s), we denote by mC the actions executed by C, mC = (mi)i∈C. The set of all possible outcomes of a move σC ∈ AC(s) at state s is defined as follows:

Definition 8 (Strategy) Given a CGS M, a strategy for a subset of players C ⊆ A is a mapping FC which associates each finite path sI , . . . , s to a move in AC(s).

A fullpath ρ is consistent with FC iff for all i ≥ 0, ρ[i+1] ∈ out(ρ[i], FC(ρ[0], . . . , ρ[i])). We denote by out(s, FC) the set of all such fullpaths ρ starting from s, i.e. where ρ[0] = s.

For each run ρ, as before we can define what it means for a norm to be enforced, and which states on a run are assigned sanction atoms. For an agent i and a path ρ, we denote the multiset of sanctions applied to i in the states on this path by sanctions(i, ρ). For a coalition C, sanctions(C, ρ) = ∪i∈Csanctions(i, ρ).

Definition 9 (Normative Update) Given a CGS M and a finite set of norms N, a normative update of M with N, M N , is a tree unravelling of M where all the norms in N are enforced (sanction atoms added to the appropriate states and paths containing states with the san⊥ atom are removed).

Definition 10 (Z-Strategy) Given a sanction bound Z, an execution path ρ ∈ out(s, FC) is Z-consistent with FC in s iff sanctions(C, ρ) ≤ Z. We denote by out(s, FC, Z) the set of all Z-consistent paths in out(s, FC) starting in s. A strategy FC is a Z-strategy in s iff out(s, FC) = out(s, FC, Z).

Given a normative update of a CGS, M N = (SN , V N , aN , δN ), the truth definition for ATLS is:

• M N , s |= 〈〈C〉〉≤Z Xφ iff there exists a startegy FC which is a Z-strategy in s such that for all ρ ∈ out(s, FC), M N , ρ[1] |= φ
• M N , s |= 〈〈C〉〉≤Z Gφ iff there exists a strategy FC which is a Z-strategy in s such that for all ρ ∈ out(s, FC), M N , ρ[i] |= φ for all i ≥ 0
• M N , s |= 〈〈C〉〉≤Z φUψ iff there exists a strategy FC Z-strategy in s such that for all ρ ∈ out(s, FC), there exists i ≥ 0 such that M N , ρ[i] |= ψ and M N , ρ[j] |= ψ for all j ∈ {0, . . . , i - 1}

In ATLS , we can express liveness and safety properties of normative updates of multi-agent systems, for example (liveness) that a group of agents can enforce φ while incurring at most sanction san, or (safety) that a group of agents cannot enforce φ while incurring less than 10 times san.

Model-Checking

The model-checking problem for a normative update to a physical multi-agent system takes as inputs the physical system M = (S, V, a, δ) with initial state sI ∈ S, a finite set of conditional norms N and a formula φ of ATLS, and returns true if M N , sI |= φ, false otherwise.

Theorem 3 The model-checking problem for a normative update of a multi-agent physical system is in PSPACE.

Proof. The proof is very similar to the proof for CTLS. To check whether a formula of the form 〈〈C〉〉≤Z φ is true in a state s, we guess C's Z-strategy from that state, prune the structure to contain only the moves which are consistent with this strategy, and then check whether a CTL formula which says that φ is true on all paths from s is true in the resulting structure. □

We provide a concrete model-checking algorithm by translating into ATL∗ + Past. ATL∗ + Past is defined as for CTL∗ + Past, but with coalition modalities instead of path quantifiers. The model-checking problem for ATL∗ + Past is decidable [Mogavero et al., 2010]. We can express in ATL∗ + Past that a path contains no more that Z sanction states, where the set of norms is restricted to norms which apply to a particular set of agents in C. The translation as before only affects modalities with sanction bounds:

where e(Z) = n1 ∗ san1, . . . , nm ∗ sanm, φ(ni+i)∗sani is a formula which says that sanction sani is applied ni + 1 or more times, and φsan⊥ is a formula which says that one of the regimented norms is violated at least once.

5 RelatedWork

The conditional norms we consider in this paper have some similarities with those proposed in [Dignum et al., 2004; Boella et al., 2008]. In [Dignum et al., 2004] obligations with deadlines are characterised in CTL using a special violation constant. However, in contrast to our norms, the obligations in [Dignum et al., 2004] are not conditional and do not have sanctions. In [Boella et al., 2008], regulative norms (without sanctions) are used to specify obligations with deadlines that are detached under specific conditions. In contrast to our work they do not evaluate norms in a temporal logic setting or consider verification.

The approach presented in this paper extends work on normative environment programming [Tinnemeier et al., 2009; Dastani et al., 2013], and can be used to analyze and reason about normative environment programs as specified in [Tinnemeier et al., 2009] and to verify that a normative update guarantees desirable system properties. In [Dastani et al., 2013], norms are represented by counts-as rules where the consequent consists of a violation atom. The norms include obligations and prohibitions, but lack conditions or deadlines. As such, they can only be used to characterize violation states (and not violation runs).

There is also a body of work on verification of normative environment programs, e.g., [Astefanoaei et al., 2009; Dennis et al., 2010]. In these approaches, norms are represented by counts-as rules characterizing violated states. The norms do not have conditions or deadlines, and sanctions are not modelled by multisets, so different violations of a norm cannot be distinguished.

Another strand of work related to our approach is [ ˚Agotnes et al., 2010], where the notion of a robust normative system is introduced. We believe that the form of normative update presented in [ ˚Agotnes et al., 2010] can be modelled in our approach by considering only regimented norms.

The framework presented in [Knobbout and Dastani, 2012] introduces different types of norm compliance and allows reasoning about agent behaviours under the assumption that the agents behave according to a specific norm compliance type. However they do not consider norm enforcement.

6 Conclusions

We define the notion of a normative update of a physical system with respect to a set of conditional norms with sanctions and deadlines. Our notion of a normative update is more complex than previous work on regimentation of a physical system or marking states or edges as violations. We extend CTL (for single agents) and ATL (for multiple agents) with sanction bounds on paths to reason about the properties of such normative updates. In particular, we can say how many sanctions the agents must incur to achieve some property. We show how to reduce the problem of verifying properties of a normative update to existing model-checking problems, and characterize its computational complexity. In future work, we plan to extend our approach to allow norms to be assigned to coalitions of agents and, moreover, redefine the enforcement of norms to allow distribution of sanctions among members of a coalition when a norm is violated by the coalition.