C+ is an action language for specifying and reasoning about the e®ects of actions and the persistence of facts over time. Based on it we present CN+, an operational enhanced form of C+ designed for representing complex normative systems and integrate them easily into the semantics of the causal theory of actions. The proposed system contains a particular formalization of norms using a life-cycle approach to capture the whole normative meaning of a complex normative framework. We discuss this approach and illustrate it with examples.
All real world domains are subject at some level to norms, be them physics, legal or social. Generically, norms de¯ne the socially accepted behavior within a society. They are an essential part of any domain, since all behavior within a domain is tied to its norms. In order to represent realistically any domain it is therefore necessary to specify those norms with the same level of detail used for the rest of the domain. Moreover, to achieve functionality norms must be speci¯ed using the same terms used to de¯ne the domain those norms regulate.
C+[
In order to produce the tools required for complex normative monitoring and reasoning, we must be able to represent more information than just the current legal state (legal, ilegal) given a normative framework. To produce operational solutions we must also be able to know the exact status of each norm (applicable, respected) in a given situation and how every action will a®ect the internal status of each norm. A system will perform better knowing which norms is it subject to and which norms is it violating by performing actions which respect the norms or which stop the system from being subject to them. To do so it is required a formalism which allows the speci¯cation of single norms, and which can express the whole variety of states a norm can be in.
In this paper we introduce a preliminary representation of norms in C+ which by the use of the same elements that de¯ne a domain is able to de¯ne the normative framework regulating it. The proposed syntax will allow the fast speci¯cation of norms, its parts and its status, in causal logic and the easy integration of those norms within the rest of the domain, contributing this way signi¯cantly to the expressiveness of C+.
The rest of the paper is structured as follows: In x2, we introduce some basic concepts of C+ which are relevant for the rest of the paper. In x3, our normative approach is introduced. In x4, we de¯ne some observable properties of our normative approach in terms of transition systems. In x5, a short overview of existing normative approaches which are related to our approach is presented. Finally, in the last section we outline our conclusions and future work. 2
C+ [
Based on that causal logic, a multivalued propositional signature is a set ¾ of symbols called constants and a nonempty ¯nite set Dom(c) of symbols ('the domain of c'), for each constant c 2 ¾, being Dom(c) and ¾ disjoint. The set ¾ of symbols can be partitioned into a set ¾f of °uent constants and a set ¾a of action constants.
An atom of signature ¾ is an expression of the form c = v ('the value of c is v ') where c 2 ¾ and v 2 Dom(c). A formula of signature ¾ is any propositional combination of atoms of ¾ linked by the propositional connectives from classical logic.
An interpretation I of ¾ is a function that assigns every constant in ¾ to an element of its domain. An interpretation I satis¯es an atom c = v (I j= c = v ) if I(c) = v. The satisfaction relation is extended from atoms to arbitrary formulas according to the usual truth tables from propositional connectives. A model of a set X of formulas is an interpretation that satis¯es all formulas in X. If X has a model it is said to be consistent or satis¯able. If every model of a set X of formulas satis¯es a formula F, it is said that X entails F (X j= F ). Two sets of formulas are equivalent if they have the same models.
A causal rule is an expression of the form: X ( Y where X and Y are formulas of ¾, called the head and the body of the rule. That causal rule can be informally interpreted as: If Y is true there is a cause for X to be true. Rules with the head ? are called constraints. A causal theory is de¯ned as a set of causal rules.
Now we de¯ne the concept of model for causal theories: Let T be a causal theory, and I be an interpretation of its signature. The reduct T I of T relative to I is the set of heads of all the rules in T whose bodies are satis¯ed by I. I is a model of T if I is the unique model of T I . Intuitively, T I is the set of formulas that are caused, according to the rules of T , under interpretation I.
Every C+ action description D of signature (¾f , ¾a) de¯nes a labelled transition system hS; A; Ri where: { S is a nonempty set of states. A state is an interpretation of the °uent constants ¾f ; S µ I(¾f ). { A is a set of transition labels, also called events or actions. An action is an interpretation of the action constants ¾a; A = I(¾a). { R is a set of labelled transitions, R µ S £ A £ S.
A state is represented by the set of °uent atoms satis¯ed in it, and it can be de¯ned as a complete and consistent set of °uent atoms. A formula 'holds' or 'is true' in a state s if s satis¯es it. An action a is said to be executable in a state s if there is a transition (s,a,s0) in R, and nondeterministic in s if there are transitions (s,a,s0) and (s,a,s00) in R such that s0 6= s00. 3
In order to integrate normative elements into C+ we need a formalization which
is coherent with its semantics. Concretely we require the formalization to be
compatible with the °uents and actions paradigm, from which can be obtained
a state-based description of norms. In [
From this approach we obtain two independent elements which fully represent the meaning of any norm, the norm's condition and the norm's content. The norm's condition de¯nes the situation requirements for a norm to be applicable or not in a given state and it contains both the activation and the deactivation condition. The second part, the norm's content, speci¯es the actions or situations the norm regulates upon and it contains the maintenance condition. For example: ² Norm:
If you drive a car under poor visibility conditions, you are obliged to use the car's headlights ² Condition: you drive a car under poor visibility conditions ² Content: you are obliged to use the car's headlights
Both the content and the condition de¯ne a set of situations in the terms of
the symbols of ¾. To do so each of them is represented by a formula of signature
¾. As an example, the previous norm could be represented by the formulae:
² Condition: drive car = > ^ visibility conditions = poor
² Content: headlights on = >
Considering those two formulae as satis¯able predicates, it can be proved whether
or not an interpretation of signature ¾ is a model of them (as seen in x2). Taking
an interpretation I of signature ¾ as the de¯nition of the world in a given
situation, by checking the satis¯ability of I in a norm's formulae we can know the
state of the norm in that situation. We can therefore obtain a norm's life-cycle
based on states, which we already explored in [
{ Respected: The norm's content is satis¯ed and therefore the norm is ful¯lled. Each of the two norm's parts can be displayed by two timelines, one representing the condition state through time and one representing the content state, so that in every moment each norm is de¯ned as active/inactive and respected/violated. A visual representation of that life-cycle can be seen in Figure 1. Since the condition and the content of a norm may or may not refer to the same elements, their respective timelines act independently through time, being a®ected di®erently by the actions happening in the world. The information regarding the current state of a norm in a given state will be given by the combined state of both elements. The fact that a norm's activation state and violation state are independent of one each other may be controversial (a norm can be violated without being active). That is further discussed and justi¯ed at the end of this section.
Condition state Content state
Inactive
u Respected u
Active Time gap with violated norm
Violated u u
Inactiv-e Respected De¯nition 1. Given a multivalued propositional signature ¾, a ¾-norm is a tuple of the form hact; resi such that act and res are two formulae of ¾f . act is called the condition of the norm and res is called the content of the norm.
The norm used previously could be represented by the next ¾-norm: n = hdrive car=> ^ visibility conditions=poor ; headlights on=>i This de¯nition of a norm can be seen from a di®erent perspective. As each of the ¾-norm's subparts is a logical formula, we can obtain a norm de¯nition based on the set of states in which the formulae of its ¾-norm are satis¯ed. Concretely a norm is composed by two sets of states, that set containing all the states where the logical formula act representing the ¾-norm condition is satis¯ed (which we will call ACT ), and that set containing all the states where the logical formula res representing the ¾-norm content is satis¯ed (which we will call RES ).
Given a multivalued propositional signature ¾, we write I¾ to denote the set of all the interpretations de¯ned over ¾.
De¯nition 2. Let n = hact; resi be a ¾-norm. A I¾-norm(n) is a tuple of the form hACT; RESi such that ACT = fIjI 2 I¾ and I j= actg and RES = fIjI 2 I¾ and I j= resg
A visual representation of De¯nition 2 can be seen in Figure 2.
From the previous de¯nitions, we can identify di®erent readings of the status of a ¾-norm regarding the states of the world and the meaning of the norm. De¯nition 3. Let n = hact; resi be a ¾-norm and I¾-norm(n) = hACT; RESi. If I 2 I¾, then the status of the ¾-norm n w.r.t. I is:
{ Active if I 2 ACT or Inactive if I 62 ACT.
And: { Respected if I 2 RES or Violated if I 62 RES.
It is important to understand the use we make of the concept violation of a norm. Since we take the condition and the content of a norm to be independent from each other, a norm can be violated without being active (which may go against some interpretations of the word violation). To represent the fact that a norm is active and violated at the same time, we introduce the concept infringed. Only in the situations where the norm is violated and active at the same time we will say the norm's status is infringed, which are the states to be considered undesirable by the norm's syntax. The states where a norm is inactive and violated do not infringe the norm, even though it may be advisable to avoid them.
De¯nition 4. Let n = hact; resi be a ¾-norm and I¾-norm(n) = hACT; RESi. If I 2 I¾, then the ¾-norm n is in a infringing status w.r.t. I if: { I 2 ACT ^ I 62 RES.
The concept of infringement gives us more information about the state of a norm and about the possible e®ects of actions. Knowing that a norm is violated but not active in a given state allows us to classify the activating actions on that state as infringing actions, since the resultant state will result in an infringed norm. The same would work for violating actions in states were the norm is active. A visual representation can be seen in Figure 3.
Condition state Inactive u Active u Inactive
Time gap with Content state Respected infringed nVoriomlated uRespecte-d
Once we have de¯ned how to specify norms in terms of formulae of the signature of a causal theory, we are in position for de¯ning the concept of a normative causal theory. = I¾.
De¯nition 5. Let T be a causal theory of signature ¾ and N¾ be a ¯nite set of ¾-norms. A normative causal theory is a tuple of the form hT; N¾i.
The concept of model of a normative causal theory is a single generalization of a model of a causal theory: Given a normative causal theory TN = hT; N¾i, if I is a model of T then I is a model of TN . The interesting part of a model I of a normative causal theory hT; N¾i is that any I 2 I¾ will always induce a particular status to every norm of N¾ since ACT [ ACT = I¾ and RES [ RES Proposition 1. Let TN = hT; N¾i be a normative causal theory. If I is a model of TN , then for each n 2 N¾, the status of n is Active or Inactive and Respected or Violated w.r.t I. 4
As was mentioned in Section 2, an action description in C+ can be regarded as a labelled transition system. In this section we are going to de¯ne some observable properties a normative causal theory adds to a labelled transition system.
The ¯rst de¯nition we introduce is a basic classi¯cation of transitions based
on the status of a ¾-norm. By lack of space, we omit to the de¯nition of an
action description of C+ (please see [
A visual representation of the states and transitions de¯ned above can be seen in Figure 4.
i:States where n is not active and respected t1:Infringing and activating transition of n ii:States where n is active and respected t2:Infringing and violating transition of n iii:States where n is infringed t3:Activating transition of n iv:States where n is not active and not respected t4:Respecting transition of n
Proposition 2. Let hS; A; Ri be a labeled transition system of an action description D and n be ¾-norm. If r1 = (s; a; s0); r2 = (s; a; s00) 2 R such that r1 and r2 are normative-di®erent, then s0 and s00 de¯ne di®erent status for n.
Essentially this proposition suggest that two normative-di®erent transitions in a transition systems necessarily get a di®erent status of a given norm. As an example of the integration of the elements and properties seen until now we will next see an example of how to formalize a norm and its involved elements in CN+. Lets consider the following norm: ............................
. .............................
If there is a standing elder or pregnant woman, you must leave them your seat. The norm formalized as in De¯nition 1, ¾-norm n=hact,resi where act (activated) and res (respected) are two logical formulas, would be represented as: n = h sitting = > ; standing elder = ? ^ standing pregnant = ? i From the previous formalization and following De¯nition 2, the set of states ACT and RES could be analyzed. Examples of the actions which would a®ect the state the ¾-norm n could be: { Activating action: sit down { Deactivating action: stand up { Respecting action: elder sit down { Violating action: appear standing pregnant { Infringing action: appear standing elder if sitting = >
In this example the set of states where the norm is active are all those where you are sitting. At the same time, the set of states where the norm is respected are those where there is no pregnant or elder person standing. Both activating actions and violating actions can be infringing actions if performed in certain situations. Sitting down when an elder is standing is an activating and infringing action, and the appearance of an elder if you are sitting is a violating and infringing action.
By representing norms this way we not only represent the content and condition
of individual norms, but also capture information regarding the reasons that
cause the infringement of a norm and the resultant states. With that knowledge
we can analyze the states related to a norm breaking event, the previous and
posterior states, and by studying the related information we can learn about
the behavior within the domain with regard to norms. Also, it is important to
note that, since CN+ de¯nes norms using the same symbols used to de¯ne the
domain, CN+ norms can be as detailed and complex as the domain itself and
can be implemented in C+ implementations, such as CCalc[
Regarding the other attempts to integrate normative elements into C+, the most
relevant ones are [
In [
Based on the norm's lifecycle introduced in x3, which captures the whole normative meaning and behavior of a given norm, the proposed sintaxis allows the representation of a complete normative framework in the terms of causal logic. By using the same tools used to de¯ne the world, CN+ can the state of a set of norms within the domain. This approach provides the basics for normative monitoring and normative reasoning, facilitating in an intuitive way the analysis of the normative situation of a state. By studying the status of all norms in a given state and how those change though time a®ected by actions, CN+ can help discover the state of norms in a future or past state. By the use of C+ expressiveness power, CN+ can formalize complex laws (as complex as the domain) making it a potentially useful tool to support decision making tasks in strongly legislated domains.
In that scope, C+ has already been used to formalize complex scenarios [
We are grateful to anonymous referees for their useful comments. This research has been partially supported by the EC founded project ALIVE (FP7-IST215890). The views expressed in this paper are not necessarily those of the ALIVE consortium.