A Dynamic Logic of Normative Systems

1 Introduction

We show that dynamic logic of propositional assignment PDL-PA provides a logical framework for normative systems, with concrete models to design rich social situations and an intuitive language to talk about institutional facts. The basic idea is that agents have a repertoire of actions to set propositional variables p to true (+p) or to false (-p). These assignments are combined by means of the standard PDL program operators of test, sequential and nondeterministic composition and iteration. We will show that PDL-PA embeds Coalition Logic of Propositional Control CL-PC [Hoek and Wooldridge, 2005].

We implement in PDL-PA an agentive and a normative dimension by supposing that the logic has special propositional variables Ai(α) and Pi(α), where i is an agent and α is an assignment. Ai(α) read as "i is able to perform α" and Pi(α) as "i is allowed to perform α". This allows to distinguish between practical possibilities (alias abilities) and deontic possibilities (alias permissions, authorizations): an agent may be able to make a propositional variable q true, but not allowed to, and the other way round. This distinction also shows up when it comes to dynamics: we have change of abilities and change of permissions. An example of the former is when the president of a university gives some amount of resources to a department. An example of the latter is when he authorizes the department to spend that money for a particular purpose. Abilities and permissions may evolve, too; We capture this in our language by assignments such as +Ai(+p), +Pi(-p), etc.

Fr´ed´eric Moisan IRIT, France

moisan@irit.fr Nicolas Troquard University of Essex, UK ntroqu@essex.ac.uk

In the logic PDL-PA we may moreover reason about higher-order abilities and permissions: agents may be able or allowed to change abilities or permissions. For example the president of the university i has the permission to authorize the vice-president j to sign a document in the name of the institution. In our language this can be written Pi(+Pj(+s)), where s denotes that the document is signed. Assignments may again modify these abilities and permissions. Beyond the (ontic and deontic) possibility to perform an action the logic PDL-PA allows to talk about the (ontic and deontic) possibility to attain a certain state of affairs. We call this the capability of an agent or a coalition of agents. (Our distinction between 'ability' and 'capability' is therefore: ability is about agents' actions, whereas capability is about outcomes that an agent can ensure.)

We introduce the basic logic PDL-PA in Section 2 and prove that satisfiability checking is PSPACE-complete. In Section 3 we embed CL-PC into PDL-PA by using a basic notion of capability. In Section 4 we provide a general analysis of different kinds of ontic and deontic abilities and capabilities (possibly of higher order). In Section 5 we provide a case study of water resource management. Finally, in Section 6 we extend PDL-PA in order to represent constitutive rules [Searle, 1969; 1995], that are essential when modelling social reality. To that end we add a binary connective leadsto to the language whose arguments are assignments and where α1 leadsto α2 reads "α1 counts as α2". We prove that satisfiability checking within that extension of PDL-PA has the same complexity as in PDL-PA. We conclude in Section 7 and discuss research avenues for future work.

2 Dynamic logic of propositional assignment

This section introduces the syntax and the semantics of the logic PDL-PA. It is basically an instantiation of propositional dynamic logic PDL [Harel et al., 2000] with concrete programs to assign propositional variables to true or false. We will show how it allows to represent and reason about abilities, permissions, and changes of abilities and permissions in multiagent systems (MASs).

2.1 Language

Assignments are expressions of the form +p or -p and modify the truth value of the propositional variable p: +p sets p to true, and -p sets p to false.

Throughout the paper, P = {p, q, . . .} is a countable set of propositional variables. The language of PDL-PA is made up of events π and formulas ϕ and is defined by the following BNF:

π Colonequal +p | -p | π; π | π ∪ π | π ∗ | ϕ? ϕ Colonequal p | ⊤ | ⊥ | ¬ϕ | ϕ ∨ ϕ | 〈π〉ϕ

where p ranges over P.

Just as in PDL, π1; π2 is sequential composition, π1 ∪ π2 is nondeterministic composition, π ∗ is iteration, and ϕ? is the test of ϕ. The formula 〈π〉ϕ reads "there is an execution of π such that ϕ is true afterwards".

The set of all assignments isA = {+p : p ∈ P}∪{-p : p ∈ P}. α, α ′ , . . . range over A. The set of all formulas is noted F , and the set of all events is noted E. We define Pϕ and Pπ to be the set of variables from P occurring in ϕ (resp. π).

The length of a formula ϕ, noted |ϕ|, is the number of symbols used to write down ϕ (without 〈, 〉, and parentheses), where the length of a propositional variable is 1. For example |〈+p〉(p ∨ q)| = 2 + 3 = 5.

The logical connectives ∧, → and ↔ have the usual meaning. The formula [π]ϕ abbreviates ¬〈π〉¬ϕ. The event skip abbreviates ⊤? ("nothing happens").

2.2 Semantics

Definition 1 A valuation V is a subset of 2 P .

The truth conditions are the customary ones for ⊤, ⊥, negation and disjunction. The dynamic operators are interpreted by means of an update relation on valuations.

V |= p iff p ∈ V V |= 〈π〉ϕ iff there is a V ′ such that VRπV ′ and V ′ |= ϕ

Rπ is a binary relation on valuations that allows to interpret events and that is defined together with |= by mutual recursion:

R+p = {(V, V ∪ {p}) : V is a valuation } R-p = {(V, V \ {p}) : V is a valuation } Rπ1 ;π2 = Rπ1 ◦ Rπ2 Rπ1∪π2 = Rπ1 ∪ Rπ2 Rπ ∗ = (Rπ) ∗ Rϕ? = {(V, V) : V |= ϕ}

A formula ϕ is satisfiable if and only if V |= ϕ for some valuation V, and ϕ is valid if and only if ¬ϕ is not satisfiable.

2.3 Complexity

The following can be proved by adapting the proofs of [Hoek and Wooldridge, 2005] and [Hoek et al., 2010].

Theorem 1 The problem of PDL-PA model checking is PSPACE-complete.

Proof (sketch). Let us first establish that model checking is PSPACE-hard. We reduce QSAT into the problem of model checking PDL-PA. Consider a quantified Boolean formula

where ϕ is a propositional formula in CNF containing no variables other than x1, . . . , xm. (If necessary an even m can be obtained by adding a dummy variable xm.) Let V = ∅ be the PDL-PA valuation over the set of propositional variables P = {x1, . . . , xm} that sets all variables to false. Let

It is readily checked that the QBF Φ is true iff V |= Φ PDL-PA . Since both the size of Φ PDL-PA and the size of the model are linear in the size of Φ, we conclude that model checking is PSPACE-hard.

The proof of membership requires the following recursive definition of the set of sequences of atomic events that are admitted by a complex event π.

adm(+p) = {+p} adm(-p) = {-p} adm(π1; π2) = {α1; α2 : α1 ∈ adm(π1) & α2 ∈ adm(π2)} adm(π1 ∪ π2) = adm(π1) ∪ adm(π2) adm(π ∗ ) = {α1; . . . ; αk : k ≥ 0 & α1, . . . , αk ∈ adm(π)} adm(ϕ?) = {ϕ?}

In the fifth line we suppose α1; . . . ; αk is skip when k = 0.

The main point in the proof is that every possible update of V by a complex event π can also be reached by a sequence that is admitted by π and that is of length at most exponential in the length of π. Precisely, it can be reached in at most 2 |π| 2 steps. This is the case despite the presence of the arbitrary iteration operator ∗ , the reason being that any π ∗ can only bring about a finite number of valuation updates.

In detail, the proof is by induction on the structure of π. The only nontrivial case is π = σ ∗ . Suppose VRσ ∗V ′ . Then there are V0, . . . , Vn such that V0 = V, Vn = V ′ and Vk-1RσVk for every k ≤ n. As Rσ ∗ is transitive we may suppose that Vk nequal Vl for k nequal l, i.e. there are no loops. By induction hypothesis σ admits α1, . . . αn such that Vk-1Rαk Vk and such that for every k, |αk| ≤ 2 |π| 2 . The sequence α = α1; . . . ; αn is admitted by π. All valuations reachable from V differ from V by the values of the variables in Pπ. Hence there are at most 2 Card(Pπ) ≤ 2 |π| such models. Notice that n cannot exceed 2 Card(Pπ) ; otherwise the sequence V0, . . . , Vn would contain loops (contradicting the previous assumption). We have:

|α| ≤ n ×maxk≤n{|αk|} + n - 1 ≤ 2 |π| × 2 |π| 2 + 2 |π| ≤ 2 (|π|+1) 2 ≤ 2 (|π ∗ |) 2

Based on that one can prove that membership of a couple of valuations (V, V ′ ) in Rπ can be decided in polynomial space. Finally one can prove that a formula ϕ can be evaluated in space polynomial in the size of ϕ; in particular, when evaluating 〈π ∗ 〉ϕ one may decide in polynomial space whether one of the (at most 2 (|π ∗ |) 2 ) valuations V ′ is accessible from V. ■

Theorem 2 The problem of PDL-PA satisfiability checking is PSPACE-complete.

Proof (sketch). Just as for model checking, hardness can be proved by encoding QBFs.

Membership can be proved as follows: given ϕ we guess a valuation V. A valuation of size polynomial in ϕ exists because we can always restrict our attention to the propositional variables occurring in ϕ. Then we check whether V |= ϕ. By Theorem 1 this can be done in polynomial time. Hence PDL-PA satisfiability can be checked in NPSPACE = PSPACE. ■

3 Embedding CL-PC

We now show that PDL-PA generalises Coalition Logic of Propositional Control CL-PC [Hoek and Wooldridge, 2005].

Let A = {i, j, . . .} be a finite set of agents. A coalition is a subset of agents J ⊆ A. We define Aϕ and Aπ to be the set of agents from A occurring in formula ϕ (resp. event π).

We suppose that beyond a set of basic propositional variables P 0 , for every i ∈ A and p ∈ P 0 there are propositional variables Ai(+p) and Ai(-p) denoting that an agent i has the ability to perform +p and -p. Assignments of variables in P 0 are called basic. Hence

Let us extend the language of PDL-PA by modal operators of ontic capability Diamond A 0 J , one for every coalition J ⊆ 2 A . The formula Diamond A 0 J ϕ reads "the agents in J are able to achieve ϕ by appropriately performing the actions in their repertoires". The truth condition is:

The language of CL-PC is built from P 0 by means of the Boolean connectives plus operators Diamond A 0 J . The class of CL-PC models is the set of PDL-PA models satisfying:

1. Ai(+p) ∈ V iff Ai(-p) ∈ V (symmetry);
2. for every α ∈ A there is i ∈ A such that Ai(α) ∈ V (exhaustivity);
3. for every α ∈ A, if Ai(α) ∈ V and Aj(α) ∈ V then i = j (exclusivity).

Theorem 3 A CL-PC formula ϕ is CL-PC satisfiable iff S ymϕ ∧ Exhϕ ∧ Exclϕ ∧ ϕ is PDL-PA satisfiable, where:

The case analysis for Exhϕ accounts for the case where a variable in ϕ is controlled by an agent not occurring in ϕ. Only the case of assignments -p is mentioned in Exhϕ and Exclϕ; the case +p follows by S ymϕ. We observe that the formulations of the three properties on CL-PC models all have length quadratic in the length of ϕ.

The above theorem says that if we extended our language by modal operators Diamond A 0 J then we could do the same kind of reasoning as in CL-PC. The next theorem says that actually we do not need to extend our language because Diamond A 0 J can already be defined in the language of PDL-PA.

Theorem 4 Let ϕ be a formula in the language of PDL-PA extended by modal operators Diamond A 0 J , for every J ⊆ 2 A . Let Pϕ = {p1, . . . , pn}. Then the formula Diamond A 0 J ϕ is PDL-PA equivalent to

In the above formula, for every variable pk occurring in ϕ there is a nondeterministic event which either does nothing (skip) or checks whether one of the agents in J can modify pk and does so. Observe that the length of that formula is linear in the length of ϕ. Therefore our language is at least as succinct as that of CL-PC.

The logic DCL-PC extends CL-PC by delegation events i p leadstoj [Hoek et al., 2010] of i transferring to j his control over p. Such an event corresponds to the following event in PDL-PA:

4 Ability, permission and capability

In this section we study various forms of ability, permission and capability. We first consider higher-order ability and permission allowing to express that an agent is able (resp. authorized) to perform a certain assignment (possibly of a propositional variable about ability or permission). We then consider the capability of an agent or a coalition of agents to ensure some outcome, distinguishing ontic and deontic capability.

4.1 Higher-order ability and permission

Let us suppose that for every p ∈ P and i ∈ A, the set P not only contains the propositional variables Ai(+p) and Ai(-p) that we have introduced in the preceding section, but also Pi(+p) and Pi(-p). Pi(+p) is read "i is authorized to make p true" (or "i has the permission to make p true"), and similarly for Pi(-p). Contrarily to the preceding section, though, we apply these constructions recursively, considering that p itself may be a special propositional variable. We can now express e.g. that i is allowed to enable j to set p to false, written Pi (+A j (-p)).

Assignments of the special propositional variables allow to model change of first-order abilities and permissions as basic assignments such as +Ai(+p) and +Pi(+p), etc. For example, +Ai(+p) makes that i can perform the action of making p true, and +Ai(-p) makes that i can perform the action of making p false; -Ai(+p) makes that i cannot make p true, and -Ai(-p) likewise, +Pi(+p) makes that i is authorized to perform the action of making p true, and so on. Beyond, assignments also allow to model change of higher-order abilities and permissions. For instance, +Ai(+Aj(+p)) makes that i can enable j to perform a certain action. For example, if i wins $100,000 in the lottery then i can give to another agent j the ability to buy a new car (by giving a part of the prize to j). +Pi(+Pj(+p)) makes that i is authorized to authorize j to perform a certain action. For example, suppose i is nominated president by the parliament. Then, qua president, i is authorized to authorize (by the act of promulgation) the minister of justice to start the process of publishing a new law in the official journal of record. +Pi(-Aj(+p)) makes that i is authorized to hinder j to perform a certain action. For example, suppose i is nominated judge at some court. Then, qua judge of the court, i is authorized to sentence some defendant j to imprisonment and, consequently, to deprive j of his freedom.

Our language accounts for the notion of normative system NSV defined as a set of permissions about the agents' behavior which belong to the valuation V, that is,

As the set of prohibitions is the complement of the set of permissions, a normative system can also be seen as a set of prohibitions about the agents' behavior. This definition of normative system therefore matches the definition accepted by several authors in the area of MASs according to whom a normative system is a set of constraints on the agents' behaviour, which may or may not be followed by the agents; see e.g. [Ågotnes et al., 2007; Shoham and Tennenholtz, 1996].

4.2 Capabilities beyond CL-PC

In Section 3 we have captured a notion of basic capability as expressible in CL-PC where one quantifies only about physical actions, viz. the assignment of basic propositional variables in P 0 . The operator Diamond A 0 J can be generalised to an operator Diamond A J quantifying over all possible assignments A:

Similarly, one may extend the language of PDL-PA by modal operators of deontic capability Diamond P J , one for every coalition J ⊆ 2 A . Diamond P J ϕ reads "the agents in J are allowed to achieve ϕ by legally performing the actions in their repertoires". In the same spirit we introduce a combined operator Diamond AP J , with the obvious reading. The truth conditions are:

V |= Diamond P J ϕ iff there are assignments α1, . . . , αn ∈ A s.t. V |= 〈α1; . . . ; αn〉ϕ, and for every αk there is i ∈ J with Pi(αk) ∈ V V |= Diamond AP J ϕ iff there are assignments α1, . . . , αn ∈ A s.t. V |= 〈α1; . . . ; αn〉ϕ, and for every αk there is i ∈ J with Ai(αk), Pi(αk) ∈ V

These operators will be handy in order to express capabilities of agents and coalitions of agents. Just as for Diamond A J they neither add expressiveness nor succinctness: there are formulas similar to that of Theorem 4 allowing to rewrite Diamond P J ϕ and Diamond AP J ϕ to PDL-PA formulas of length polynomial in the length of ϕ. Therefore complexity of reasoning with such operators stays in PSPACE.

5 An example: managing water resources

This section illustrates an application of the logic PDL-PA in a concrete normative system of water management.

There are two farmers f1 and f2 working in a certain area close to a town called Thirstytown who need water in order to irrigate their fields. In this area there are three different exploitable water basins 1, 2 and 3. Only water basins 1 and 2 can be safely used by the farmers; basin 3 provides drinkable water to the population of Thirstytown, and if it is exploited for irrigation then Thirstytown will fall short of water. There are two other actors in this scenario: c is the chief of the Water Authority which has the jurisdiction over the area, and p is a local policeman working in Thirstytown.

The propositional variables {b1, b2, b3} indicate whether the level of water in a given basin is high or low: b1 means that "the level of water in the basin 1 is high", ¬b1 means that "the level of water in the basin 1 is low", etc. Furthermore, for every farmer i ∈ { f1, f2} and for every propositional variable bh with h ∈ {1, 2, 3}, Ai(-bh) expresses that basin h is physically connected to the field of farmer i so that i is able to exploit the water of the basin h, and Pi(-bh) expresses that i is authorized to exploit the water of basin h.

We suppose that the initial situation INIT is defined by the conjunction of the following six facts, characterized by the formulas ϕ1, . . . , ϕ6 of Table 1:

1. The farmers can legally only exploit basins 1 and 2 but not basin 3 (formula ϕ1).
2. Farmer f1 has access to basins 1 and 2, but not to basin 3 (formula ϕ2).
3. Farmer f2 has access to basin 3, but not to basin 1 and 2 (formula ϕ3).
4. The chief of the Water Authority is able to authorize the policeman of Thirstytown to add and remove connections between basins and fields (imagine that a connection between a basin and a field can be added or removed by opening or closing a sluice gate) (formula ϕ4).
5. The chief of the Water Authority is authorized to authorize the policeman of Thirstytown to add and remove connections between basins and fields (formula ϕ5).
6. The policeman of Thirstytown is able to add and remove the connections between basins and fields, but is not authorized to do that (formula ϕ6).

The problem to be solved is to find an executable and authorized procedure such that, given the initial situation INIT, it ensures that the situation GOAL will be achieved, where GOAL is defined by the conjunction of the following two facts ψ1 and ψ2.

1. Every farmer has exclusive control over at least one basin in {1, 2}: each farmer's field is connected to at least one water basin in {1, 2} which is not connected to the other farmer's field. Formally:

1. No field is connected to basin 3: ¬Af1 (-b3) ∧¬Af2 (-b3). Let α + i,h = +Pp(+Ai(-bh)) and α - i,h = +Pp(-Ai(-bh)), and πi,h = α + i,h ; α - i,h be the event of the policeman getting authorization to connect/disconnect the field of farmer i to basin h.

Now, consider the following sequence of events.

1. The chief of the Water Authority authorizes the policeman to modify the connections between basins and fields. Formally: π1 =

1. The policeman removes the connection between basin 1 and f1's field. Formally: π2 =

1. The policeman adds the connection between basin 1 and f2's field. Formally: π3 =

1. The policeman removes the connection between basin 3 and f2's field. Formally: π4 =

It can be shown that the formula

expresses that the policeman has the ontic capability to guarantee that no farmer has access to basin 3.

The formula INIT → Diamond AP {c} GOAL however is invalid: the chief cannot ensure GOAL alone. In contrast, the formula INIT → Diamond AP {c,p} GOAL is valid, meaning that the policeman and the chief can cooperate to achieve the goal.

6 Integrating constitutive rules

According to several authors working in legal theory and in the field of normative MASs (see, e.g., [Alchourr´on and Bulygin, 1971; Boella and Torre, 2004]), normative systems are based both on regulative as well as constitutive (i.e. nonregulative) components. That is, normative systems are not only defined in terms of sets of permissions, obligations, and prohibitions (i.e. norms of conduct) but also in terms of rules which specify and create new forms of behavior and concepts. According to Searle for instance "[. . . ] regulative rules regulate antecedently or independently existing forms of behavior [. . . ]. But constitutive rules do not merely regulate, they create or define new forms of behavior" [Searle, 1969, p. 33]. In Searle's theory [Searle, 1969; 1995], constitutive rules are expressed by means of "countsas" assertions of the form "X counts as Y in context C" where the context C refers to the normative system in which the rule is specified. Constitutive rules relate "brute" physical facts, actions, etc. with institutional facts, actions, etc. For example, in the US, receiving a piece of paper with a certain shape, color, etc. (a physical action) counts as receiving a five-dollar bill (an institutional action). 1

While our logic PDL-PA allows to model and reason about some regulative aspects of normative systems (permissions and authorizations), it does not account for constitutive rules which are an essential component to the modelling of social reality. In this section, we show how PDL-PA can be extended in order to describe them.

1 We only consider here the "counts-as" relation between events. We note that Searle's "counts-as" relation is also between objects (such as pieces of paper and money).

We postpone to future work an analysis of more subtle aspects of "counts-as" like for instance the relationship between "counts-as" and the notion of institutional power, and the distinction between the "counts-as" relation and a notion of dependence between events in the causal sense as in [Thielscher, 1997]. Note that the distinction between "counts-as" and causality is somehow explicit in Goldman's theory of action [Goldman, 1970] where "causal generation" is opposed to "conventional generation". According to Goldman, physical actions are causally generated, that is, they just consist in an agent bringing about (i.e. causing) a certain state of affairs to be true. On the other hand, institutional actions are conventionally generated, by which he meant that actions such as signalling before making a turn, and checkmating one's opponent, exist in virtue of rules or conventions relating physical actions with institutional effects.

We add to the language a primitive α1 leadsto α2 that reads that the occurrence of α1 counts as the occurrence of α2, where α1 and α2 are assignments. For example, suppose we are modelling driving laws. Then, the formula +80mph leadsto +overspeed means that if a car runs at 80mph this counts as an overspeeding that has to be sanctioned. (We abstract away from the institutional context in which the constitutive rule applies.) Technically, our modelling is inspired from Thielscher's solution to the ramification problem in reasoning about actions [Thielscher, 1997].

Definition 2 A model with constitutive rules is a tuple (V,C) such that V is a valuation and C ⊆ A × A is a reflexive and transitive relation over assignments that satisfies the following coherence constraint:

When (α1, α2) ∈ C then the occurrence α1 counts as the occurrence of α2. The constraint (Coh) says that an event cannot have inconsistent ramifications. Note that it follows from (Coh) together with reflexivity of C that (+q, -q) nelement C, (+Pi (α), -Pi(α)) nelement C, etc.

Remark 1 It is worth noting that there is some disagreement whether the "counts-as" relation should satisfy transitivity. For a discussion on this matter see [Jones and Sergot, 1996; Grossi et al., 2006; Lorini et al., 2009]. In addition, some authors argue that the "counts-as" should satisfy contraposition [Grossi et al., 2006], while others have a different opinion on this matter [Jones and Sergot, 1996]. We did not include contraposition in the list of properties of Definition 2; however, the constraint "if (+p, +q) ∈ C then (-q, -p) ∈ C" could be added to C.

The truth condition for the "counts-as" construction is:

We have to modify the definition of the relation Rπ in order to take the relation C into account; we only change the case where π is an atomic event α:

Note that we are now able to define Rα without a case analysis as we did previously. Note also that C is never updated.

We note the new logic PDL-PAleadsto. Validity and satisfiability in PDL-PAleadsto are defined in the standard way. For example, the following schemas are valid:

α leadsto α (α1 leadsto α2) ∧ (α2 leadsto α3) → (α1 leadsto α3) ¬ ((α leadsto +q) ∧ (α leadsto -q)) 〈α〉q ↔ ((α leadsto +q) ∨ (q ∧ ¬(α leadsto -q)))

The last equivalence is reminiscent of Reiter's successor state axioms in the Situation Calculus [Reiter, 2001]. It follows from it that (α leadsto +q) → 〈α〉q. For example, if driving at 80mph counts as overspeeding (i.e. +80mph leadsto +overspeed) then, after starting to drive at 80mph, the driver will be over the speed limit (i.e. 〈+80mph〉overspeed).

The proofs of the complexity results for PDL-PA can be adapted straightforwardly to PDL-PAleadsto.

Theorem 5 The problems of model checking and of satisfiability checking in PDL-PAleadsto are both PSPACE-complete.

7 Conclusion

We have presented the propositional dynamic logic of assignments PDL-PA, with assignments of the form +p and -p that are combined by the standard program constructions of PDL. The logic allows to reason about practical possibilities (alias abilities) and deontic possibilities (alias permissions) of agents and coalitions of agents, as well as the dynamics of abilities and permissions. The abilities and permissions may be higher-order. We have demonstrated the logic on an example about water resource management. Finally, we have introduced an extension of PDL-PA that allows to reason about constitutive rules.

We have shown that the model checking problem and the satisfiability problem are PSPACE-complete, both for PDL-PA and its extension with the "counts-as" operator. This contrasts with other formalisms that were proposed in the literature. In most of them complexity results are not mentioned. The only complexity result we are aware of are by Ågotnes et al. In [Ågotnes et al., 2007] a normative extension of CTL is presented. Its symbolic model checking problem is proved to be PSPACE complete in the interpreted case, and EXPTIME hard in the uninterpreted case. In the former, agents' abilities and permissions are completely specified, while in the latter only the abilities are completely specified. In that respect, symbolic model checking in our logic provides more flexibility. We note however that their framework has a richer temporal ontology than ours. We leave further investigation of differences and similarities to future work.

A prominent benefit of our dynamic logic evaluated over simple symbolic models is that their extension with further notions relevant to social reality appears like a simpler task than in any other formalism of the literature. We have demonstrated that with the integration of constitutive rules. An interesting direction of future research that we did not address in Section 6 is the dynamics of constitutive rules in an institution. This could be done in a way that is in the very spirit of this paper by integrating two new kinds of events: π1 + π2

adds π2 as a ramification of π1, and π1 - π2 withdraws π2 as a ramification of π1. The only difficulty here is to design a model update preserving the constraints on C. This is subject of ongoing work.