(PDF) A Deontic Action Logic with Sequential Composition of Actions

A deontic action logic with sequential composition of actions ⋆ Piotr Kulicki and Robert Trypuz John Paul II Catholic University of Lublin, Al. Raclawickie 14, 20-950 Lublin, Poland {kulicki,trypuz}@kul.pl http://www.kul.pl Abstract. We start our investigations from the deontic action model de- fined in multi-situation settings. Then we discuss the validity of formulas constructed in a language with a finite number of basic actions, parallel and sequential compositions of actions, a free choice operator and the standard deontic operators of obligation, strong permission and prohibi- tion. The main achievements of the paper are definitions of metalogical counterparts of deontic operators and interpretation function of actions taking into account their terminating and non-terminating executions. Key words: deontic action logic, sequential composition of actions, ter- minated and non-terminated actions Introduction In the early eighties of the twentieth century through the works of Segerberg [9] and Meyer [7], deontic logic went back to von Wright’s initial idea of study- ing of the deontic properties in relation to actions. The results of our research, described in the works [13, 12, 11, 10], contributed to better understanding of deontic action logic systems, especially those based on finite Boolean algebra. Boolean algebra in the systems in question was treated as a simple theory of actions providing a precise meaning for such action constructors as action com- plement, intedeterministic choice between actions and parallel execution. In all of the systems we have proposed until now, we have taken into account only one-step actions. We could say that so far we have studied deontic theories of a single situation or state. Two systems described in [13, 10] are an exception, whose interpretation was provided in the structures containing situations. How- ever, the situations in the structures were not connected. In the present paper we want to extend the semantics of our systems on transitions between situations and extend the language of our deontic action logic with sequential composition of actions. The new framework poses very interesting and challenging questions concerning the deontic characteristics of sequences of actions. For instance, what ⋆ The project was funded by the National Science Center of Poland (DEC- 2011/01/D/HS1/04445). 2 Piotr Kulicki, Robert Trypuz does it really mean to impose a regulation on someone “you ought to do α and then β” or “you are allowed to do α and then β”, taking into account that action α can be carried out in several ways, some of which may exclude the possibil- ity of executing β afterwards. Sequences of actions (as fragments of computer programs) are widely studied in computer science by means of such formalisms as Kleene algebra, propositional dynamic logic (PDL) (in which Boolean and Kleene algebras are the essential components) or Hoare logic [5, 3, 4]. Those sys- tems show their usefulness the in analysis of algorithms, programs and more general phenomena of agents’ behaviour. They were also connected with deontic notions in e.g. [7, 2, 14, 1] and recently [8]. Especially the last article presents an approach similar to the one adopted by us in this paper. Its authors, Prisacariu and Schneider, build a deontic action logic on the foundation of an algebraic structure which they call synchronous Kleene algebra. The structure combines parallel and sequential execution of ac- tions and a free choice operator on actions. The deontic characteristics of complex actions, including multi-step actions, is defined on the basis of deontic values of simple state-to-state transitions. The model they use, however interesting and inspiring, we find at some points unintuitive. Also the fact that they assume algebra of actions independently from model-theoretic structure and then define the model for algebraically defined normal form is unusual in logic. Moreover, they use the notion of compensation which is inseparably connected with pro- hibition and obligation, which is very interesting by itself, but makes it difficult to extract the fundamental properties of prohibition and obligation1 . Thus, we propose an alternative system based on our earlier works, especially [13]2 . In section 1 we start our investigations with introducing the deontic action model defined in multi-situation settings. We put forward the recursive defini- tions of metalogical counterparts of deontic operators. Then, in section 2, we discuss the validity of formulas. We propose the interpretation function of ac- tions taking into account their terminated and non-terminated executions. 1 Fundamentals of deontic action logic with sequential composition of actions 1.1 Basic intuitions The basic elements which we will use to build a formal model for deontic action logic is a representation of two types of entities: actions and states (situations). In any reasonable formalisation of action theory, at least some of the actions results in a transition between situations. Two question arise 1 In the present paper we are only interested in the study of the relation of deontic operators to various operators on actions, especially sequential composition. There- fore we ignore the issues concerning the results of actions, especially sanctions that can be captured by PDL. 2 Unfortunately, due to space limitation, there is no systematic comparison of our approach with the work of Prisacariu and Schneider. We leave that comparative study for further works. A deontic action logic with sequential composition of actions 3 1. Should the same actions performed in the same situation always result in the same transition(s) of situations? 2. Is it possible that a transition between the same two states is a result of carrying out two or more different actions? The answer to those depends on the notion of action and the granularity of description. In the present paper we only assume positive answer for the first of the above questions. To remain a consequent deontic action logicians we have to connect deontic notions with actions both in the syntax and in the formal semantics. This dis- tinguishes our approach from the majority of others, in which, in a more or less explicit form, semantics connects permitted, forbidden and obligatory actions with the respective deontic characteristics of states that are their outcomes. As we have mentioned in the introduction, in this paper we are mostly in- terested in studying sequentially composed actions. They are constructed from single-step actions. An important issue is that such complex actions may be un- successful in two ways, which have to be formalised differently. One is that a first step of an action is impossible in a given situation. The other occurs when an action can be started but, after some part of it is performed, it cannot be continued in the state that was reached3 . We express our intuitions first in a form of a model-theoretic structure. A semantic characterisation of our logic is based on the following frame: DAS = hS, E, T , LEG, ILL, REQi, where S is a nonempty, finite set of situation (or state) types, E is a nonempty, finite set of basic action types used for cross-situation identification of actions (we shall think about elements of 2E as more general action types), T is a set of action steps, understood as action descriptions (one can also think about elements of that set as elementary labelled transitions between states) and LEG, E ILL, REQ are functions from S to 22 , representing actions legal, illegal and required in a specific state, respectively. The first three elements of DAS form its action part, the remaining ones form its deontic part. 1.2 Action part of the model Let us first discuss the action part. Every element of T is a triple hs1 , s2 , ei, where s1 , s2 ∈ S are initial and final states respectively and e ∈ E is the label of an action causing a transition from s1 to s2 . Intuitively subsets of T represent different ways of performing actions. We can represent a parallel execution of two actions by the intersection of respective sets of elementary transitions and a free choice between two actions by their sum. 3 We have introduced the concepts of external (successful) and internal (unsuccessful) actions in the context of deontic notions in [13]. Relevant reference to a logical study of attempts and successful actions is [6]. 4 Piotr Kulicki, Robert Trypuz We impose on DAS the so called functionality restriction (cf. [1]), i.e. for any s, s, s′′ , e if hs, s′ , ei ∈ T and hs, s′′ , ei ∈ T , then s′ = s′′ . However it may happen in DAS that hs, s′ , ei ∈ T and hs, s′ , e′ i ∈ T , for some s, s′ , e, e′ such that e 6= e′ . The set of all action steps executable in state s will be referred to by “exe(s)” and defined as follows: exe(s) , {hs, s′ , ei : hs, s′ , ei ∈ T } (1) To model actions that are sequentially composed of other actions we have to introduce a notion of transition, which grasps the intuitive notion of a sequence of action steps. A transition is a triple hs1 , s2 , Ei, where s1 , s2 ∈ S and E ∈ E ∗ , i.e., E is a finite, possibly empty, sequence of action labels from E. E represents a sequence of actions of fixed types that should be performed consecutively to move from state s1 to state s2 . More formally we can define the notion of transition (i.e., sequence of action steps) in DAS inductively in the following way: – For any s ∈ S a triple hs, s, []i, where [] denotes an empty sequence of action types, is a transition. – If hs1 , s2 , Ei is a transition and hs2 , s3 , ei is an action step from T then hs1 , s3 , E ′ i, where E ′ is a result of adding label of action type e at the end of sequence E, is also a transition. We shall use symbol T ∗ for the set of transitions constructed from action steps from T . Let us notice that in general in the notion of transition we do not record intermediate states. For example if there exist elementary transitions: hs1 , s2 , e1 i, hs1 , s3 , e1 i, hs2 , s4 , e2 i, hs3 , s4 , e2 i from T , transition hs1 , s4 , [e1 , e2 ]i does not determine a specific path in the structure of states since it is not specified which of the intermediate states s2 or s3 is used. Since one-step actions are represented by sets of elementary transitions, an arbitrary action is represented by a set of non-elementary transitions. Indeed, one-step actions should more precisely be represented by transitions with a se- quence of label of the length 1 (one-step transitions). We can define a sequential composition of sets of transitions. Let T1 and T2 be sets of transitions defined in DAS. Then4 T1 ◦T2 , {hs1 , s2 , Ei | ∃s3 (hs1 , s3 , E1 i ∈ T1 & hs3 , s2 , E2 i ∈ T2 ) & E = E1 k E2 }, In the similar ways as we have defined exe, we define now function “exe∗ ” as a set of transitions executable in some situation: exe∗ (s) , {hs, s′ , Ei : hs, s′ , Ei ∈ T ∗ } (2) Below we define six functions. The first four of them return sets of transitions satisfying certain properties. The last two have their ranges in the sets of action types and situation types respectively5 . rem(T, s1 , s2 ) = {hs2 , s′ , Ei : ∃e hs1 , s2 , ei ∈ T &hs1 , s′ , [e|E]i ∈ T } (3) 4 Symbol k stands for a concatenation of sequences. 5 Expression “[e|E]” in the functions below is syntactic sugar meaning [e]||E. A deontic action logic with sequential composition of actions 5 init(T, s) = {e : ∃s′ , E hs, s′ , [e|E]i ∈ T } (4) fso(T, s) = {s′ : ∃e ∈ init(T, s), E hs, s′ , ei ∈ T } (5) beg(T ) = {hs1 , s2 , E1 i ∈ T ∗ : ∃s3 , E2 , E (hs1 , s3 , Ei ∈ T & E1 k E2 = E)} (6) max(T ) = {t ∈ T : ∀t′ ∈ T (t ∈ beg({t′ }) =⇒ t′ = t)} (7) f in(T1 , T2 ) = {hs1 , s2 , Ei : hs1 , s2 , Ei ∈ T1 & ¬∃s3 , E ′ hs2 , s3 , E ′ i ∈ T2 } (8) “rem(T, s1 , s2 )”, read “remainders of a set of transitions T with respect to an initial state s1 and the first step outcome s2 ”, returns a set of transitions that are obtained from those transitions from T starting from s1 for which s2 is a first step outcome by removing their first steps. Initial action steps of a set of transitions in a certain state (init) is a function ∗ which arguments are sets of transitions from 2T and states from S and value is a set of action steps from 2E . Intuitively the function returns a set of action types that are attached to all possible initial steps of transitions from T in state s. Finally, “fso” (“first step outcomes of a set of the results of initial transitions ∗ in a certain state”) is a function which arguments are sets of transitions from 2T and states from S and value is a set of states from 2S . Intuitively the function returns a set of states that are reachable from state s by a first step of a transition from T . Function “beg” provides sets of initial fragments (beginnings) of transitions from T . The initial fragments in concern do not have to be proper, so T ⊆ beg(T ). Function “max” selects from a set of transitions T a subset containing only maximal elements, in the sense that no proper initial fragment of such an element can also be an element of the resulting set. Function “f in” gives a subset of its first argument (T1 ) containing elements that do not have a continuation in the function’s second argument (T2 ), in other words, the elements of the set that is the value of the function “f in” finish after T1 . 1.3 Deontic part of the model Let us now turn to the deontic part of the model. For each situation s ∈ S values of the functions for s: LEG(s), ILL(s) and REQ(s) should be understood as sets of sets of action types that are respectively legal, illegal and required in s. We have introduced and characterised properties of the functions in question in [12, 11] in the context of single-step actions. For expressing deontic properties of the actions, set of action types E sufficed and transitions appeared to be unnecessary. That is why LEG(s), ILL(s) and REQ(s) have been defined as E functions from S to 22 . Below we briefly review properties of LEG(s), ILL(s) and REQ(s). We find them simple and intuitive and want to treat them as a base for defining deontic properties of sequences of actions later on. 6 Piotr Kulicki, Robert Trypuz Properties of LEG(s), ILL(s) and REQ(s) for action types For any s ∈ S and X, Y ∈ 2E , LEG(s) and ILL(s) are ideals, i.e., they satisfy the following principles: X ∈ LEG(s) & Y ⊆ X =⇒ Y ∈ LEG(s) (9) X ∈ LEG(s) & Y ∈ LEG(s) =⇒ X ∪ Y ∈ LEG(s) (10) X ∈ ILL(s) & Y ⊆ X =⇒ Y ∈ ILL(s) (11) X ∈ ILL(s) & Y ∈ ILL(s) =⇒ X ∪ Y ∈ ILL(s) (12) For any s, LEG(s) and ILL(s) have only empty set in common: LEG(s) ∩ ILL(s) = {∅} (13) A necessary condition for two elementary transitions to be required is that their intersection should be required too: X ∈ REQ(s) & Y ∈ REQ(s) =⇒ X ∩ Y ∈ REQ(s) (14) An impossible action is never required: ∅ 6∈ REQ(s) (15) For any state s ∈ S required actions are legal: REQ(s) ⊆ LEG(s) (16) There is no state s ∈ S in which all transitions starting from it are illegal: exe(s) 6∈ ILL(s) (17) If X is an action required in s and its intersection with action Y is empty, then Y is illegal in s: X ∈ REQ(s) and X ∩ Y = ∅ =⇒ Y ∈ ILL(s) (18) We can now shift the functions LEG, ILL and REQ to define legal, illegal and required sets of transitions. Let us use symbols LEG ∗ , ILL∗ and REQ∗ respectively for the new functions transforming the states from S into subsets ∗ of 2T . The functions are defined as below. By the definitions a set of transitions T is legal (required) when in each reachable state the set of all action steps defined by T is legal (required or empty) and is illegal when each transition from T contains an illegal step. Note that since REQ is not empty REQ∗ is also not empty. A deontic action logic with sequential composition of actions 7 Properties of LEG ∗ , ILL∗ and REQ∗ for transitions Let T be a set of transitions and s a state. T ∈ LEG ∗ (s) iff the following two conditions hold: (i) init(T, s) ∈ LEG(s), (ii) for any s′ ∈ fso(T, s), rem(T, s, s′ ) ∈ LEG ∗ (s′ ). T ∈ ILL∗ (s) iff ∀t ∈ T t ∈ ILL∗1 (s), where ILL∗1 is a function such that t = [e|E] ∈ ILL∗1 (s) iff one the following two condition holds: (i) {e} ∈ ILL(s) or (ii) for any s′ such that hs, s′ , ei ∈ T , E ∈ ILL∗1 (s′ ). T ∈ REQ∗ (s) holds when the following two conditions hold: (i) init(T, s) ∈ REQ(s) or init(T, s) = ∅, (ii) for any s′ ∈ fso(T, s), rem(T, s, s′ ) ∈ REQ∗ (s′ ). The above definitions cause the values of the functions LEG ∗ , ILL∗ and REQ∗ (for any state as their arguments) to inherit most properties imposed on the values of functions LEG, ILL and REQ. Thus for any state s ∈ S we have: T1 ∈ LEG ∗ (s) & T2 ⊆ T1 =⇒ T2 ∈ LEG ∗ (s) (19) T1 ∈ LEG ∗ (s) & T2 ∈ LEG ∗ (s) =⇒ (T1 ∪ T2 ) ∈ LEG ∗ (s) (20) ∗ ∗ T1 ∈ ILL (s) & T2 ⊆ T1 =⇒ T2 ∈ ILL (s) (21) ∗ ∗ ∗ T1 ∈ ILL (s) & T2 ∈ ILL (s) =⇒ (T1 ∪ T2 ) ∈ ILL (s) (22) ∗ ∗ REQ (s) ⊆ LEG (s) (23) ∗ ∗ exe (s) 6∈ ILL (s) (24) Let us just sketch the proofs of the above properties. (19) holds by (9) since init(T2 ) ⊆ init(T1 ), fso(T2 , s) ⊆ fso(T1 , s) and, for any s′ ∈ fso(T2 , s), rem(T2 , s, s′ ) ⊆ rem(T1 , s, s′ ). (20) holds by (10) since init(T1 ∪ T2 ) = init(T1 ) ∪ init(T2 ), fso(T1 ∪ T2 , s) = fso(T1 , s) ∪ fso(T2 , s) and, for any s′ ∈ fso(T1 ∪ T2 , s), rem(T1 ∪ T2 , s, s′ ) = rem(T1 , s, s′ ) ∪ rem(T1 , s, s′ ). (21) and (22) are obvious. For (23), since the definitions of LEG ∗ and REQ∗ are analogous, it is enough to notice that ∅ ∈ LEG. For (24) it is enough to notice that a set of one-step transitions that are based on action labels that are not illegal in s (the set is not empty by (17)) is not a member of ILL∗ (s). Thus, by (21), it is not a member of exe(s), either. Moreover we have additional property concerning transition with empty se- quence of labels hs, s, []i for any s: hs, s, []i ∈ REQ∗ (s) (25) 8 Piotr Kulicki, Robert Trypuz ∅ ∈ REQ∗ (s) (26) It has to be emphasised that the following counterpart of property (14) does not hold: T1 ∈ REQ∗ (s) & T2 ∈ REQ∗ (s) =⇒ (T1 ∩ T2 ) ∈ REQ∗ (s) (27) 2 Logic 2.1 Formal language The basic language of DAL is defined in Backus-Naur notation in the following way: ϕ ::= α ⊜ α | P(α) | F(α) | O(α) | ¬ϕ | ϕ ∧ ϕ (28) α ::= skip | 0 | ai | α ⊔ α | α ⊓ α | α; α (29) where ai belongs to a finite set of basic actions (or in other words action genera- tors) Act0 , “0” is the impossible action, “α ⊔ β” – α or β (a free choice between α and β); “α ⊓ β” – α and β (parallel execution of α and β); “α ⊜ β” means that α is locally (i.e. in fixed situations) identical with β (instead of ¬(α ⊜ β) we will also write α 6⊜ β); “P(α)” – α is (strongly) permitted; “F(α)” – α is forbidden, “O(α)” – α is obligatory. Further, for fixed Act0 , by Act we shall understand the set of formulae defined by (29). 2.2 Satisfaction in the model Intuitively any action from Act is interpreted in a model as a set of transitions. We restrict the interpretation in such a way that the interpretation of an action always contains all transitions possessing the same sequence of labels or contains none of them. That is because labels are used for (trans-state) identification of actions – elementary transitions with the same label represent the same agent behaviour possibly in different states. In particular single-step actions (basic actions and their combinations achieved by the use of operators ⊓ and ⊔ or, in other words, actions which do not contain sequential composition) are interpreted as sets of single-step transitions. When we come to multiple-step actions we consider transitions that represent full actions, from the beginning to the end of the action, henceforward transitions terminal for the action, and transitions that represent only the beginning of the action and cannot lead to the end of it — transitions non-terminal for the action. The latter occur when a transition realising an initial part of the action finishes in a state in which the remaining part of the action cannot be carried out. ∗ Formally we represent terminal (tm : Act −→ 2T ) and non-terminal (nt : ∗ Act −→ 2T ) transitions as two separate sets. A deontic action logic with sequential composition of actions 9 Interpretation function for terminal transitions hs1 , s2 , Ei ∈ tm(ai ) =⇒ ∀s′1 , s′2 hs′1 , s′2 , Ei ∈ tm(ai ) (30) tm(skip) = {hs, s, []i : s ∈ S} (31) tm(0) = ∅ (32) tm(α ⊔ β) = tm(α) ∪ tm(β) (33) tm(α ⊓ β) = tm(α) ∩ tm(β) (34) tm(α; β) = tm(α) ◦ tm(β) (35) For non-terminal transitions the situation is more complicated since they be- have less nicely in the context of the same operations on actions. Interpretation function for non-terminal transitions Assuming that t(α) = tm(α) ∪ nt(α) interpretation function for non-terminal transitions is defined as follows: nt(ai ) = nt(skip) = nt(0) = ∅ (36) nt(α ⊔ β) = max((nt(α) − beg(tm(β))) ∪ (nt(β) − beg(tm(α)))) (37) nt(α ⊓ β) = max(beg(t(α)) ∩ beg(t(β))) − beg(tm(α) ∩ tm(β)) (38) nt(α; β) = nt(α) ∪ f in(tm(α), t(β)) ∪ (tm(α) ◦ nt(β)) (39) Condition (36) states that one-step actions, skip and 0 cannot be started and non-terminable. Condition (37) states that non-terminal transitions of free choice of actions α and β consists of non-terminal transitions of α and β that are not the beginnings of terminating transitions of β and α respectively. Func- tion max eliminates from the resulting set non-maximal elements to maintain uniqueness. Condition (38) constructs nt(α ⊓ β) as a set of maximal common beginnings of terminal and non-terminal transitions connected with α and β that are not terminating. Finally, condition (39) states that the set of non-terminal transitions of α; β consists of non-terminal transitions of α, elements of tm(α) that do not have a continuation in β and non-terminal transitions of β attached as a continuation to β. Let us notice that an element of nt(α) cannot be an initial fragment of any element of tm(α), formally: nt(α) ∩ beg(tm(α)) = ∅ (40) Finally, interpretation is a function into a pair of sets of transitions. It is defined as follows: I(α) = htm(α), nt(α)i (41) 10 Piotr Kulicki, Robert Trypuz Providing tm(α, s) = tm(α)∩exe∗ (s) and nt(α, s) = nt(α)∩exe∗ (s), by I s (α) we understand a local interpretation of an action, i.e., interpretation relativised to some situation s, and define it as follows: I s (α) = htm(α, s), nt(α, s)i (42) Now we are ready to formulate satisfaction conditions for a formula of DAL in state s of model M. Satisfaction conditions M, s |= P(α) ⇐⇒ I s (α) = htm(α, s), nt(α, s)i & tm(α, s) ∪ nt(α, s) ∈ LEG ∗ (s) M, s |= F(α) ⇐⇒ I s (α) = htm(α, s), nt(α, s)i & tm(α, s) ∈ ILL∗ (s) M, s |= O(α) ⇐⇒ I s (α) = htm(α, s), nt(α, s)i & tm(α, s) 6= ∅ & nt(α, s) = ∅ & tm(α, s) ∈ REQ∗ (s) M, s |= α ⊜ β ⇐⇒ I s (α) = I s (β) M, s |= ¬ϕ ⇐⇒ M, s 6|= ϕ M, s |= ϕ ∧ ψ ⇐⇒ M, s |= ϕ & M, s |= ψ For a permitted action we require that both terminal and non-terminal tran- sitions are legal. For forbidden action it is enough that terminal transitions are illegal because impossible actions are illegal anyway. For obligatory actions we require that such an action cannot be unsuccessfully started, so the set of non- terminal transitions has to be empty. Obligatory actions have to be possible, so the set of terminal transitions has to be non-empty. Of course transition sets for all states have to be required. The concepts of satisfiability, validity and tautology are defined in standard way. 2.3 Toy example Imagine that each students of art of some university during his/her studies is obliged to go to a city where there is a gallery or museum where the painting Lady with Ermine is currently exhibited and see it (and obviously write an essay about it). Let us also assume that the painting is currently exhibited in Cracow. Let us take into account a deontic action structure consisting of five types of action e1 , . . . , e5 and the transitions between states s1 , . . . , s6 defined as it is illustrated in figure 1. Let us also assume the following deontic characteristics of actions: {e1 , e2 , e3 } ∈ LEG(s1 ), {e5 } ∈ LEG(s3 ), {e4 } ∈ LEG(s4 ) and {e2 } ∈ REQ(s1 ), {e5 } ∈ REQ(s3 ). Now we add the following actions to the deontic action logic: – a – go to a city where there is a gallery or museum with great paintings – b – go to Cracow A deontic action logic with sequential composition of actions 11 nna s2 Vie l to ra ve =t e1 e2 = travel to Cracow e5 = see the painting of Lady with Ermine s1 e 3 =t s3 s6 rav el to Pa ris e4 = see the painting of La Gioconda s4 s5 Fig. 1. Actions in Kripke structure – c – see the paining of Lady with Ermine – d – see the paining of La Gioconda and provide their interpretations as follows: – I(a) = h{hs1 , s2 , [e1 ]i, hs1 , s3 , [e2 ]i, hs1 , s4 , [e3 ]i}, ∅i – I(b) = h{hs1 , s3 , [e2 ]i}, ∅i – I(c) = h{hs3 , s6 , [e5 ]i}, ∅i – I(d) = h{hs4 , s5 , [e4 ]i}, ∅i – I(b; c) = h{hs1 , s6 , [e2 , e5 ]i}, ∅i – I(b; d) = h∅, {hs1 , s3 , [e2 ]i}i – I(a; c) = h{hs1 , s6 , [e2 , e5 ]i}, {hs1 , s2 , [e1 ]i, hs1 , s4 , [e3 ]i}i We show for example that M, s1 |= P(b; c). So M, s1 |= P(b; c) ⇐⇒ I s1 (b; c) = h{hs1 , s6 , [e2 , e5 ]i}, ∅i&{hs1 , s6 , [e2 , e5 ]i} ∈ LEG ∗ (s1 ). To be sure that {hs1 , s6 , [e2 , e5 ]i} ∈ LEG ∗ (s1 ) we must check whether the following two facts hold: (i) init({hs1 , s6 , [e2 , e5 ]i}, s1 ) ∈ LEG(s1 ) and (ii) for any s′ ∈ fso({hs1 , s6 , [e2 , e5 ]i}, s1 ), rem({hs1 , s6 , [e2 , e5 ]i}, s1 , s′ ) ∈ LEG ∗ (s′ ). It is easy to check that init({hs1 , s6 , [e2 , e5 ]i}, s1 ) = {e2 }. Because {e2 } ⊆ {e1 , e2 , e3 }, by assumption that {e1 , e2 , e3 } ∈ LEG(s1 ) and principle (9) we know that {e2 } ∈ LEG(s1 ). Because fso({hs1 , s6 , [e2 , e5 ]i}, s1 ) = {s3 }, we must only check whether rem({hs1 , s6 , [e2 , e5 ]i}, s1 , s3 ) = {hs3 , s6 , [e5 ]i} ∈ LEG ∗ (s3 ). And once again to answer whether {hs3 , s6 , [e5 ]i} ∈ LEG ∗ (s3 ) we have to check two conditions: (i) init({hs3 , s6 , [e5 ]i}, s3 ) ∈ LEG(s3 ) and (ii) for any s′ ∈ fso({hs3 , s6 , [e5 ]i}, s3 ), rem({hs3 , s6 , [e5 ]i}, s3 , s′ ) ∈ LEG ∗ (s′ ). Because init({hs3 , s6 , [e5 ]i}, s3 ) = {e5 }, we obtain that init({hs3 , s6 , [e5 ]i}, s3 ) ∈ LEG(s3 ). Then we have that fso({hs3 , s6 , [e5 ]i}, s3 ) = {s6 }. So, rem({hs3 , s6 , [e5 ]i}, s3 , s6 ) = ∅ ∈ LEG ∗ (s3 ), which finishes the proof. 12 Piotr Kulicki, Robert Trypuz In a similar way we check that M, s1 |= O(b; c). Note that satisfaction con- dition for “O” requires in this case that nt(b; c, s1 ) = ∅. One can easily check that M, s1 6|= O(a; c), because I s1 (a; c) = I s1 (htm(a; c, s1 ), nt(a; c, s1 )i) and nt(a; c, s1 ) = {hs1 , s2 , [e1 ]i, hs1 , s4 , [e3 ]i} = 6 ∅. This shows that the norms of obli- gation for sequences of actions should be specified in our approach in such a way that at each step of sequence execution, carrying out a step-action cannot exclude the possibility of successful termination of the sequence. 2.4 Identity of actions Let us now list some important tautologies of the system. First, let us consider equations between actions6 . Monoid axioms for “⊔” and “0” (associativity and left-right identity): (α ⊔ β) ⊔ γ = α ⊔ (β ⊔ γ) (43) α⊔0=0⊔α =α (44) Monoid axioms for “;” and “skip” (associativity and left-right identity): α; (β; γ) = (α; β); γ (45) α; skip = skip; α = α (46) Commutativity axiom for “⊔”: α⊔β =β⊔α (47) “;” distributes over “⊔” on both the left and right: α; (β ⊔ γ) = (α; β) ⊔ (α; γ) & (α ⊔ β); γ = (α; γ) ⊔ (β; γ) (48) 0 is the left annihilator for “;”: 0; α = 0 (49) Idempotency axiom for “⊔”: α⊔α=α (50) It is worth mentioning in this place that structure (Act, ⊔, ; , 0, skip) does not form idempotent semiring, because 0 is not the right annihilator for “;”, i.e., the formula (which is e.g. an axiom of Kleene algebra): α; 0 = 0 is not a tautology. Additionally we have idempotency, commutativity and asso- ciativity axioms for “⊓”, distributivity “⊓” over “⊔” and absorption: α⊓α=α (51) 6 We will write α = β when, for each state s in each model M, M, s |= α ⊜ β A deontic action logic with sequential composition of actions 13 α⊓β =β⊓α (52) (α ⊓ β) ⊓ γ = β ⊓ (α ⊓ γ) (53) α ⊓ (β ⊔ γ) = (α ⊓ β) ⊔ (α ⊓ γ) (54) (α ⊓ β) ⊔ β = β & α ⊓ (α ⊔ β) = α (55) Weak distributivity of “⊓” over “;” also holds: If α, β do not contain “;”, then (α; γ) ⊓ (β; δ) = (α ⊓ β); (γ ⊓ δ) (56) Formula (56) corresponds to an axiom of synchronous Kleene algebra from [8]. To verify that (43)—(56) are indeed tautologies, one has to check that both sides of tautologies have the same values of functions tm and nt. For tm it is quite an easy observation. For nt it is not obvious, but the proofs can be obtained by routine, though complex, algebraic transformations, for which we do not have room in the present paper. Equations (43)—(56) allow us to transform each ac- tion to an equivalent action in the normal form defined below. Normal form of an action Any action of a from: a1 ⊓ . . . ⊓ an , where a1 , . . . an ∈ Act0 (n ≥ 1) is a quasiatom. Action skip and any action of the form: α1 ; . . . ; αn , where α1 , . . . αn−1 (n ≥ 1) are quasi-atoms and αn is a quasiatom or 0 is a sequent. An action is in the normal form iff it is a free choice of sequents, i.e. has the form: α1 ⊔ . . . ⊔ αn , where α1 , . . . αn (n ≥ 1) are sequents. Theorem 1. For any action α there exists action β in the normal form such that α = β. Proof. To prove the theorem it is enough to use distributivity laws (48), (54) and (56), and absorption law (55). 2.5 Deontic laws Let us now turn to deontic laws. The laws specific for deontic operators without sequential composition and skip are as follows: P(α ⊔ β) ≡ P(α) ∧ P(β) (57) F(α ⊔ β) ≡ F(α) ∧ F(β) (58) 14 Piotr Kulicki, Robert Trypuz O(α) → P(α) (59) ¬(O(α) ∧ F(α)) (60) To see that formula (57) is valid, it is enough to recall that tm(α ⊔ β) = tm(α) ∪ tm(β) and notice that nt(α ⊔ β) ⊆ beg(t(α) ∪ t(β)) and nt(α) ∪ nt(β) ⊆ beg(t(α ⊔ β)). Thus, by satisfaction condition for P (57) is valid. The validity of (58) and (59) follows immediately from satisfaction conditions for F, O and P and properties (22) and (23) respectively. To see that (60) is valid let us suppose α is obligatory in state s. Then, for s, tm(α) 6= ∅ and tm(α) ∈ REQ∗ (s) ⊆ LEG ∗ (s). Thus, for any t ∈ tm(α) each action label must be an element of respective REQ(s′ ) ⊆ LEG(s′ ). But LEG(s′ ) and ILL(s′ ) are disjoint for any state. Thus, t cannot contain an illegal fragment and consequently ¬F(α). Basic laws with sequential composition or skip are as follows: O(α; β) → O(α) (61) F(α) → F(α; β) (62) P(α; β) → P(α) (63) O(skip) (64) P(α) → P(α; 0) (65) F(α; 0) (66) ¬O(α; 0) (67) The validity of (61)—(67) follows directly from the satisfaction conditions for P, F and O. Most of them are self-explanatory. One may find puzzling the co-occurrence of (65) and (66) since some actions are at the same time permitted and forbidden. All of these actions are not executable as a whole sequence (and therefore they are forbidden) but all of their elements are permitted (so they are permitted). We believe that formulas (43)—(67) with the rules of Modus Ponens and Substitution constitute a complete axiomatisation of the system, however a proof of that fact is left as future work. Among their consequences are: P(skip) (68) P(α) → P(α ⊓ β) F(α) → F(α ⊓ β) (69) P(0) F(0) ¬O(0) (70) The following formulas, which are true for one-step actions (see [12]) are not tautologies in general: F(α) ∧ P(α) → α ⊜ 0 (71) O(α) ∧ O(β) → O(α ⊓ β) (72) O(α) ∧ α ⊓ β ⊜ 0 → F(β) (73) A deontic action logic with sequential composition of actions 15 Conclusion and future perspectives We have presented a deontic action model defined in multi-situation settings as a generalisation of a single-step model. Within the model we have discussed deontic properties of actions with sequential composition. The model enables us to treat actions from the language as prescriptions or plans that an agent can realise step-by-step (not analysing the whole model at the beginning) and be sure that each step of a permitted action is permitted and each way of starting an obligatory action allows to continue such an action to its end. To achieve that goal we have introduced the interpretation function for actions that takes into account their terminating and non-terminating executions. The system can be easily extended by imposing additional conditions on the model (e.g. determinism of actions outcomes) or by enriching the language with negation modalities and PDL operators. References 1. Pablo F. Castro and T.S.E. Maibaum. Deontic action logic, atomic boolean algebra and fault-tolerance. Journal of Applied Logic, 7(4):441–466, 2009. 2. F. Dignum, J.-J.Ch. Meyer, and R.J. Wieringa. Free choice and contextually per- mitted actions. Studia Logica, 57(1):193–220, 1996. 3. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194–211, 1979. 4. C. A. R. Hoare. An axiomatic basis for computer programming. COMMUNICA- TIONS OF THE ACM, 12(10):576–580, 1969. 5. Stephen C. Kleene. Representation of events in nerve nets and finite automata. Automata Studies, 1956. 6. Emiliano Lorini and Andreas Herzig. A logic of intention and attempt. Synthese, 163(1):45–77, 2008. 7. J.J. Meyer. A different approach to deontic logic: Deontic logic viewed as variant of dynamic logic. Notre Dame Journal of Formal Logic, 29(1):109–136, 1987. 8. Cristian Prisacariu and Gerardo Schneider. A dynamic deontic logic for complex contracts. The Journal of Logic and Algebraic Programming, 81:to appear, 2012. 9. Krister Segerberg. A deontic logic of action. Studia Logica, 41:269–282, 1982. 10. Robert Trypuz. Simple theory of norm and action. In Anna Bro˙zek, Jacek Jadacki, ˇ and Berislav Zarni´c, editors, Theory of Imperatives from Different Points of View, Logic, Methodology and Philosophy of Science at Warsaw University 6, pages 120 – 136. Wydawnictwo Naukowe Semper, 2011. 11. Robert Trypuz and Piotr Kulicki. A systematics of deontic action logics based on boolean algebra. Logic and Logical Philosophy, 18:263–279, 2009. 12. Robert Trypuz and Piotr Kulicki. Towards metalogical systematisation of deontic action logics based on boolean algebra. In Proc. 10th International Conference Deontic Logic in Computer Science, volume 6181 of Lecture Notes in Computer Science. Springer, 2010. 13. Robert Trypuz and Piotr Kulicki. A norm-giver meets deontic action logic. Logic and Logical Philosophy, 20:59–72, 2011. 14. Ron van der Meyden. The dynamic logic of permission. J. Log. Comput., 6(3):465– 479, 1996.