Towards a formal definition of electronic contracts

Department of Informatis

Towards a Formal

Denition of Eletroni

Contrats 1

Researh Report No.

348

Cristian Prisaariu

Gerardo Shneider

Isbn 82-7368-305-2

Issn 0806-3036

January 2007

Contrats

†

Cristian Prisaariu

‡

Gerardo Shneider

§

January 2007

Abstrat

In this paper we propose a formallanguage for writing eletroni

ontrats, based on the normative deonti notions of obligation, pro-

hibition, and permission. We take an ought-to-do approah, where

the abovenotions areappliedto ationsinsteadofstate-of-aairs. We

propose an extension of the

µ

^{-alulus in order to apture the intu-}

itivemeaningofobligation,prohibitionandpermission,andtoexpress

deterministi and onurrent ations. We provide a translationof the

ontratlanguageintothelogi,andweshowhowthesemantisfaith-

fully aptures the meaning of the ontrat language. We also show

how our language aptures most of the intuitive desirable properties

of eletroni ontrats, as well as how it avoids most of the lassial

paradoxes of deontilogi. We alsodisuss informally themainprob-

lemsin formalizingtheabove normative deonti notions in partiular

intheontextofeletroniontrats. Wenallyshowitsappliability

on aontrat example.

†

Partiallysupportedby theNordunet3 projetContrat-OrientedSoftwareDevelop-

mentforInternetServies.

‡

Dept. ofInformatisUniv. ofOslo, P.O. Box1080Blindern, N-0316Oslo,Norway.

E-mail: ristii.uio.no

§

Dept. ofInformatisUniv. ofOslo, P.O. Box1080Blindern, N-0316Oslo,Norway.

E-mail: gerardoi.uio.no

1 Introdution 3

2 Obligation, Permission and Prohibition: Informal Disus-

sion 7

2.1 On theTruth-Valueand the NotionofConsisteny inDeonti

Logi . . . 7

2.2 Conjuntion inAtion Logis . . . 8

2.3 On the Relationship Between Obligationand Permission . . . 9

2.4 Obligations and Permissions . . . 10

2.4.1 About Disjuntion of Ations . . . 10

2.4.2 About Conjuntion of Ations . . . 11

2.4.3 About the Negation of Ations . . . 13

2.5 On Obligation, Permission and Prohibition inE-ontrats. . . 13

3 Puzzles and Paradoxes 15 3.1 ClassialParadoxes and Puzzles . . . 16

3.2 A new paradox? . . . 18

4 Desirable Properties of a Language for Contrats 19 5 A Speiation Language for Contrats 21 5.1 Ation Algebra . . . 21

5.2 Ation Normal Formal . . . 23

5.3 The Contrat Language . . . 23

6 The Underlying Logi for the Contrat Language 29 6.1 Propositional

µ

^{-alulus: Syntax and Semantis . . . . . . . . 29}

6.2 Yetanother propositional

µ

^{-alulus . . . . . . . . . . . . . . 31}

6.3 Translatingthe languageintothe logi . . . 34

7 Properties of the Contrat Language 36 7.1 Paradoxes . . . 39

8 Example 41 9 Other Approahes 44 10 Conlusion 46 10.1 Further Work . . . 46

Withthe imminentuse ofInternetasameansfordevelopingross-organiza-

tionalollaborationsand virtualommunitiesengaged inbusiness, new hal-

lengesarise toguaranteeasuessfulintegration andinteroperabilityofsuh

virtualorganizations. Servie-orientedarhitetures(SOA)isbeomingmore

and more the trend in this arena. Entities partiipating in a SOA have no

aess toomplete information,inludinginformationfor hekingthe relia-

bilityoftheservieproviderand/orservieonsumer. Forinstane,aservie

onsumer has no aess to the ode implementing the servie, and is there-

fore unabletoexamine,muh less verify, the servieimplementationto have

assurane of its ompliane with his/her needs. This motivates the need

of establishing an agreement before any transation is performed, through

a ontrat, engaging all partiipants in the transation under the ommit-

mentsstipulatedinsuhadoument,whihmustalsoontainlausesstating

penalties in ase of ontrat violations. In the ase of a bilateral ontrat,

one usually talks about the roles of servie provider and servie onsumer;

but multi-lateralontrats arealsopossible wherethe partiipantsmay play

other roles. A servie provider may also use a ontrat template (i.e. a

yet-to-be-negotiatedontrat)topublishthe serviesit iswillingtoprovide.

As a servie speiation, a ontrat may desribemany dierent aspets of

a servie, inludingfuntional properties and also non-funtionalproperties

likeseurity and quality of servie (QoS).

Beforeaontratissignedithastogorstthroughastageofnegotiation.

Atthis stage,the ontrattemplateoered by theservie providerhas tobe

analyzed(e.g. bymodelhekingtehniques) andhangedtosuite theneeds

of both the lient and the provider. After eah hange the new ontrat is

sent to the other party whih either aepts it or hanges it again. This

proess goesonuntil anagreement isahieved.

In order toadvane towards a reliable SOA, weneed tobeable to write

ontrats whih an be understood by the software engaged in the negoti-

ation proess,and latermay beused by virtualorganizationsresponsiblefor

ensuring that the ontrat is respeted. In other words, ontrats should be

amenable to formalanalysis.

Formal Approahes for Contrats. There are urrently several dier-

ent approahes aiming at dening a formal language for ontrats. Some

works onentrate on the denition of ontrat taxonomies [Aag01, BJP99,

TP05 ℄, while others look for formalizations based on logis (e.g. lassi-

al [DKR04℄, modal [DM01℄, deonti [GR06, PDK05℄ or defeasible logi

[Gov05, SG05℄). Other formalizationsare based on models of omputation

In our opinion, the most promising approah is the one based on logi.

A logi for ontrats not neessarily has to be based on, or extend, deonti

logi, but must ontain normative deonti notions (obligation, permission,

and prohibition) and preserve their intuitive properties, both in the proof

system and inits modeltheory.

Deonti Logi. Formalizing the usual notions of obligation, permission

and prohibition is not an easy task as witnessed by the extensive researh

onduted by the deonti ommunity both from the philosophial and the

logial point of view, starting as early as 1926 [Mal26℄

1

. These works have

obviouslybeen donemuhbeforethe onrete problemofdening eletroni

ontrats(e-ontrats)and theproblemsidentiedstillontinue tohallenge

philosophers, logiiansand omputer sientists.

In early papers (e.g. [Wri51℄) the approah was to relate the normative

notions of obligation, permission and prohibition in a similar way as the

quantiers (all,some,no) and modalities(neessary, possible,impossible)of

lassial and modal logi, respetively. This was the bases of the so-alled

Standard DeontiLogi(SDL)whihisbuiltonlassialpropositionallogi,

leading toa nie formalizationbut alsoto many paradoxes.

One of the rst issues totake into aount before formalizingnormative

notions is whether we want to represent (names of) human ations or (sen-

tenesdesribing)states ofaairs,produtofahumanation. Theformeris

usually known asanought-to-doandthe latterasought-to-be. The following

is a lassial example where One ought to build a window an be under-

stoodas anought-to-dosentene, while Thereought tobe a window is an

ought-to-besentene. Inmanyasesitispossibletotranslateanought-to-be

sentene into its orresponding ought-to-do quite easily, as in the following

example: It ought to be the ase that John pays the money to Smith

(ought-to-be) and John ought to pay the money to Smith (ought-to-do).

In manye-ontratsitismore naturaltondought-to-do statements;where

the subjet isstatedexpliitly(the supplier,thelient),theations (thatare

permitted or forbidden) are visible, and also in many ases there might be

an objet. There may be also ases where an ought-to-be approah gives a

moreoniseexpression, likeinQoSontratswherewemayhavestatements

that express quantitative restritions like: The average bandwidth should be

more than 20kb/s. The disussion among philosophers and logiians is far

fromanend inwhat onerns thedeisionofwhether one approahisbetter

1

Mally'sworkis onsidered apreursorof deontilogi, thoughitis widely aepted

that moderndeontilogistartedwiththeworkbyG.H.AvonWright[Wri51℄.

Some authors have osillated from one side to the other von Wright for

instane took anought-to-beapproahinearlypapers,and laterinlinedfor

the ought-to-do (ation-based) approah,as stated in[Wri99℄.

Notethat norms(and lausesin ontrats), by denition,are violable(if

wehavetheguaranteethatnobodywillviolatethenorms,normativesystems

would beompletelyuseless). Hene,ontrary-to-duty obligations(orCTDs)

and ontrary-to-prohibitions (orCTPs), onerning the fatthat obligations

mightnotbefullledandthat prohibitionsmightbeviolated,are important

aspets to be onsidered. In both ases, we might want to know whih is

the reparation or the penalty to be applied. See for instane [PS96℄ for a

disussion onCTDs.

Therearemanyotherproblemstobeonsideredwhenformalizingobliga-

tion, permissionand prohibition. Among others,their interrelation (duality

and denitionintermsofeahother),theunderstandingof theirtruth-value

(even thedisussion whetheritisreasonable totalkabout the truth-valueof

suh notions),and the dierenebetween must and ought.

The intention ofthis setionisto give anoverview of the main problems

in deonti logi, and not to disuss the dierent solutions. See [Wri99℄ for

a nie overview of the history,problems and dierent approahes ondeonti

logi. Theentry DeontiLogi of theStanford Enylopedia ofPhilosophy

ontains a general desription of the topi, mainly the dierent paradoxes

arising under SDL 2

. See also the hapter of MNamara in the Handbook of

the Historyof Logi [MN06 ℄.

Our Approah and Contributions. The above disussion should not

givetheimpressionthatwearetryingtosolveanoldunsolvableproblem. We

are mainlyonernedwith formaldenitionofontrats,and morepreisely,

of e-ontrats. Bynarrowing thesopeofappliationof deontilogi, weare

denitelyon aterrainwheremanyof the philosophialproblems ofthe logi

are not present.

Inthispaperwetakearststeptowardsthedenitionofaformalontrat

language, based on an extension of the

µ

^{-alulus. Our starting point is}

[BWM01 ℄, where a x-point haraterization of obligation, permission and

prohibition is given, based on the modal

µ

^{-alulus. The logi allows to}

expressobligation,permissionandprohibitiononregularations,takingthus

an out-to-do approah.

The main ontribution of this paper is the denition of a ontrat lan-

guage with the followingproperties:

2

http://plato.stanford.edu/entries/logi-deonti/index.html.

2. It is possible to express in the language obligations, permission and

prohibition over onurrent ationskeeping their intuitivemeaning;

3. Obligation of disjuntive and onjuntive ations is dened omposi-

tionally;

4. It is possible toexpress CTDs and CTPs;

5. The language has aformalsemantis given inavariant ofthe proposi-

tional

µ

^-alulus.

Other side ontributions are:

1. We revisit the relations between the deonti notions, providing new

insightonhowthey shouldberelatedunderthe ontextof e-ontrats;

2. We give speial attention to the disjuntion on obligations, to whih

we provide anatural and preiseinterpretation;

3. Weextend the propositional

µ

^{-aluluswith the} possibilityof express- ing onurrent and deterministiations.

The paper is organized as follows. In Setion 2 we present an informal

disussion about deontilogi, and the main problems arising when formal-

izing the notions of obligation,permission and prohibition. In Setion 3 we

present the most well-known paradoxes as well as a new one we found un-

der ertain dierent interpretation of the normative deonti notions. Based

on the two previous setions we present a list of desirable properties for a

ontratlanguage, inSetion4. In Setion5wepresent ourformallanguage

for writingontrats,and inSetion6wepresent avariantof the

µ

^-alulus,

with itssyntaxandsemantis,and wegiveatranslationof thelanguageinto

the logi. In Setion7we showthat ourlanguageavoidsthe mostimportant

paradoxes, and that itsatises most of the desirableproperties desribed in

Setion 4. In Setion 8 we present an example of a ontrat written in our

language. We briey desribe a related approah also based on a variant

of the

µ

^{-alulus [BWM01 ℄ in Setion 9 and we disuss the advantages and}

disadvantages of the approah in ontrast to ours. We onlude in Setion

10.

formal Disussion

Capturing the rightintuitionof normativenotionsin general,and inparti-

ular of obligation,permissionand prohibition,is adiulttask. Wepresent

in this setion an informal disussion about the main ideas to take into a-

ount when trying to formalize the above notions. In what follows we use

O(a)

^{to denote the obligation of performing a given ation}

a

^{, similarly for}

permission(

P (a)

^{) and} prohibition (

F (a)

^{), and}

+

^{for hoie among ations.}

A more preise denition willbe given later.

2.1 On the Truth-Value and the Notion of Consisteny

in Deonti Logi

Thissetionisentirelybasedon[Wri99℄. Inthephilosophialtraditionofvon

Wright's eduation, norms were seen as subjetive, relative and dependent

on ulture, without any truth-value: norms, as presriptions for ondut,

simply are not true or false [Wri99℄. The apparent problem here is that

if one takes this point of view, then it is not possible to study the logial

relationbetween obligation,permissionand prohibition,todeneanotionof

logial onsequene or todetet ontraditions. Von Wright argues that the

aboveonlyimpliesthatlogiismuhmorethantruthandthusnormsarestill

subjet tologial laws. Von Wrightmakesa dierene between presriptive

and desriptivesentenes. In the former thesentene does not have atruth-

value, it only enuniates a norm, while in the latter it has a truth-value (it

is a norm-proposition). In itsdesriptive interpretationof formulas, deonti

logi should aimata omplete and ontradition-freesystem of norms. Von

Wrightmakesaleardistintionbetweenought,the obligation,andmust,

the pratial neessity. The rst is neither true nor false and itis an ought-

to-be, while the seond an be true or false depending on the situation and

is thus relatedto something whih has to bedone (ought-to-do).

Von Wright laims that a set of norms is onsistent if and only if, the

onjuntionofallstatespronounedobligatorybythenormswithanyoneof

the states pronouned permitted is a doable state of aairs, i.e., something

whih an be ahieved through human ation. Alongthese lines, it is pos-

sible to denethe notion of normative entailment: a onsistent set of norms

entailsanother oneif and onlyif addingthe negationof thelatter makesthe

set inonsistent.

φ φ s

a

b

t’

t

Figure1: Example of a modelfor

haiφ ∧ hbiφ

^{but not for}

ha&biφ

^.

2.2 Conjuntion in Ation Logis

Before explaining why onjuntion is problemati when ombined with de-

ontioperators,westart by showing someproblems whentrying toadd on-

juntiontoPropositionalDynamiLogi(PDL).Ifwewanttodene

ha&biφ

ompositionally,itis naturalto thinkthat it an be dened as follows:

ha&biφ = haiφ ∧ hbiφ.

If ations

a

^and

b

^are interpreted as sets of pairs of states (i.e. relations overstates)and ifonjuntionoverations

a&b

^isinterpretedasintersetion of sets [BV03℄ then in PDL extended with ation onjuntion (denoted as

P DL ^∩

^{) it holds only that}

ha&biφ ⇒ haiφ ∧ hbiφ

^{. The onverse impliation}

doesnot hold in

P DL ^∩

^{beause the leftside meansthatthere exists astate,}

say

t

^{to whih the system may get by performing ation}

a

^{and also by per-}

forming ation

b

^{and the formula}

φ

^{holds in}

t

^{. On the other hand,the right}

side means that there exists a state

t

^{to whih one may get by performing}

ation

a

^{andthereexistsanotherstate}

t ^′

^{towhihonemaygetbyperforming}

ation

b

^{, andinboth}

t

^and

t ^′

^,

φ

^holds;but

t

^and

t ^′

^{maybedierent. Beause}

of these the right side does not imply the left side. Consider the model in

Figure1whihisamodelfor theformulaonthe rightofthe impliationbut

is not a model for the formulaon the left of the impliationbeause itdoes

not exist a state to whih the system an get by performing both ations

a

and

b

^.

Onesolutiontothe aboveproblemisnot todene

h·i

^and

[·]

^ononjun-

tion of ations, but to axiomatize the logi giving the desirable properties

[BV03℄. Anothersolution istoenhane the logi with nominals asinhybrid

logis (see for instane [AtC06℄ and referenetherein). Hybridlogis dene,

besidesthe sort of propositionalvariables,anew sort of speial propositions

alled nominals NOM

= {i, j, k, . . .}

^{disjoint from the set of} propositional variables. The intent of the nominals is to name states of a model. The

namingofthe statesispossiblebeauseeahnominalholdsinonlyonestate

b a

t s

φ,i

Figure2: Example of amodelfor both

haiφ ∧ hbiφ

^and

ha&biφ

^.

of the model (i.e. if a nominal

i

^{holds in the state}

s

^{of the model then it}

is said that the state has the name

i

^{; alsothere an not be anotherstate}

s ^′

with the same name

i

^{). Given aurrent state, if}

i

^{isthe name ofa suessor}

state, then we ould write:

hai(i ∧ φ) ∧ hbi(i ∧ φ) ⇒ ha&bi(i ∧ φ),

whihwould forethe transitions tohave the samesoure and targetstates.

A model for both formulas on the left and right of the impliation arrow is

pitured in Figure 2. This, however, does not fore the two ations to be

performedonurrently. Inordertoapturetrue onurrenywewouldneed

to fore having only one transition labeled with

a

^and

b

^{in an atomi way;}

we willsee asolution inSetion 6. An extension of PDL with nominalswas

rst presented in [PT85℄(see also [PT91℄).

2.3 On the Relationship Between Obligation and Per-

mission

Therelationbetweenobligationandpermissionisratherumbersome. There

is no onsensus on how to relate these two notions or if it is possible (or

more preisely, natural) to express one in terms of the other. Many re-

searhers argue for dening permission as derived from obligation (or vie-

versa):

O(a) ≡ ¬P (a)

^{. In[Wri99℄,vonWrightarguesfornotusingtheabove}

denition, though he introdued it in his early works; he proposes instead

the following two equivalenes:

¬O(a) ≡ P (a)

^and

O(a) ≡ ¬P (a)

^.

Welaimthatnoneof theaboveequivalenesarenatural,atleast forour

purpose in trying todene a logi forformalizing e-ontrats.

First notie that not being obliged to do something does not add any

knowledge about what is permitted. Furthermore, in the ontext of a logi

for ontrats it does not make muh sense to talk about negation of obli-

gations: a ontrat must speify your rights and obligations, not what you

are not obliged to do. Thus the rst equivalene above an be disarded.

Furthermore, we donot aeptthe impliation

¬P (a) ⇒ O (a)

^{beause itis}

ation isprohibited) that itisobligatory toperform the negated ation. On

the other hand,

O(a) ⇒ ¬P (a)

^{might bereasonable only onsystems where}

the preseneof

O(a)

^and

O(a)

^{makethesystem}inonsistent. Noteverybody agrees onsuh inonsisteny,so we donot onsider itin a rst instane.

In ouropinion the onlynatural relationsbetween obligationand permis-

sion are the following:

O(a) ⇒ P (a)

O(a) ⇒ ¬P (a)

⁽¹⁾

wheretheseondimpliationonlyholdsifthereisnoontrary-to-dutyobliga-

tion(CTD) assoiatedwith

O(a)

^{,inwhihaseonemusttakethereparation}

in ase the obligationis not fullled.

2.4 Obligations and Permissions

2.4.1 About Disjuntion of Ations

We rst make a remark about obligation over disjuntion of ations. Many

papers use the notation

O(a ∪ b)

^{for obligation of disjuntion of ations,}

while infat they mean hoie, or exlusive or. Indeed, it does not seem

very intuitive to dene obligation of lassial disjuntion of ations, sine

this is not the usual meaning in natural languages. We will, thus, use the

notation

a + b

^{for the hoie of ations.}

Wewanttodene

O(a + b)

ompositionallywhileavoidingthe Rosspara- dox. In order todo so,we need to havea hierarhial denition of formulas

and not allowthe

∨

^{onobligationformulas. Insteadweadd aXORoperator}

(

⊕

^{)overobligationformulastorepresentthe intuitiveideaofhoie3. Inthis}

way we have the intuitivemeaningof the obligationof ahoie:

O(a + b) = O(a) ⊕ O(b).

Many of the problems assoiated with the hoie disappear as soonas a

temporal aspet is introdued [PS96℄, as for example in "You must pay on

time or at least give a notie 10 days before the paying date. If you don't

pay ontime and youdon't givenotie, you must pay ane of 1000$".

3

This operator is notnew to logis: it anbe dened in lassialpropositionallogi

andalsohasspeialpropertiesinlinearlogi.

We would like to be able to express obligation of performing onurrent

ations,

O(a&b)

^{. There are two solutionsto do this: (1) using} interleaving, and (2) having true onurreny. True onurreny would apture the idea

that

O(a) ∧ O(b) ⇒ O(a&b)

^{. Wewillpropose latera solutionbased onsets}

of ations toapture onurrent ations inthe logi

Another important aspet to take into aount is the dierenebetween

permissionand obligation over onjuntion of ations. Saying that you are

obliged to remain silent and to talk with your lawyer introdues an inon-

sisteny sinethereisarequirementtodotwoontraditoryations. On the

other hand,tosay that youhave the right toremainsilentand totalkwith

your lawyer does not introdues any inonsisteny. This shows that there

is a lear dierenebetween permissionand obligationof onjuntion of a-

tions. We believe the disussion about the dierenes between onjuntion

under permissionand underobligationsisonstrutiveand sheds some light

on problems not always onsidered by many researhers.

We onsider now the problemof understanding

¬O(a&b)

^{4. We will give}

here three dierent interpretations. We then justify the intuitive solution,

and then explain how we an get the right solution by making a distin-

tion between the onjuntion of ations under the sope of obligations and

permissions.

1. By dening

¬O(a) = P (a)

^{, we get (by applying De Morgan law and}

the equivalene

O(a&b) ≡ O(a) ∧ O(b)

^):

¬O(a&b) = ¬(O(a) ∧ O(b)) = ¬O(a) ∨ ¬O(b) = P (a) ∨ P (b)

This is ompletely ounter-intuitive sine it is not lear what the dis-

juntion over permissions means. We also have disjuntion onobliga-

tions,whihwebelieveshouldbeforbiddensyntatially,thoughmany

researhers ondeontilogi see disjuntion onobligationsasnatural.

2. One an argue that

¬O(a) = P (a) ∧ P (a)

^{, sine} intuitively not being obliged to do something gives you permission to do the ontrary, but

alsothe permissionof the positiveation itself. In this ase we have:

¬O(a&b) = P (a) ∧ P (b) ∧ P (a) ∧ P (b)

Wehavenowtwodierentinterpretations(basedontheinterpretation

P (a&b) = P (a) ∧ P (b)

^or

P (a + b) = P (a) ∧ P (b)

⁾

4

Notie that the disussion aboutnegation of obligationsis more philosophial, and

inluded hereonly for ompleteness. As disussed in theprevious setion negationover

obligationsisnotnaturaline-ontrats.

(a)

¬O(a&b) = P (a&a&b&b)

(b)

¬O(a&b) = P (a + a + b + b)

The rst optionseems more natural,but this wouldimplytogivespe-

ialmeaning tothe &, sine intuitively

a&a =⊥

^under obligation,but

a&a 6=⊥

^under permission. The seond option has the problem that we annot do two things at the same time (like

a&b

^{, whih should be}

allowed).

Allthe disussion above lead usto the followingonlusions:

1. The ation operator& behaves dierently under permissions and obli-

gations, hene we need two dierent ation operators (let's all them

& o

^and

& p

^).

2. Weneed to introdue XOR alsofor permissions.

3. Wemust allownegationon ationsalso underpermissions.

Assuming we have a onit relation

♯

^{between ations, in what follows}

we propose some laws for gettingthe above:

1.

& o

^{an only be used under} obligations and must have the following properties:

a& o a =⊥

a& o b =⊥

^if

a♯b (a& o b) = a& o b

Wethen have that:

O(a& o b) =⊥

^if

a♯b O(a& o a) =⊥

O(a& o b) = O(a) ∧ O(b)

¬O(a& o b) = ¬O(a) ∧ ¬O(b) = P (a&b)

2.

& p

^{an only be used under} permissions and must have the following properties:

a& p a = a + a

a& p b 6= a + b

^if

a 6= b ∧ ¬(a♯b)

a& p b → a + b

^if

a♯b

^(Here

→

^{means that}

a& p b

^{must be replaed}

by

a + b

⁾

¬(a& p b) = a& p b

P (a& p b) = P (a) ∧ P (b)

^if

¬(a♯b) P (a& p a) = P (a + a) = P (a) ⊕ P (a)

P (a& p b) = P (a + b) = P (a) ⊕ P (b)

^if

a♯b P (a& p b) = F (a) ∧ F (b)

Withthese laws, wemight get the rightinterpretationof the

¬O(a&b)

^.

2.4.3 About the Negation of Ations

Negation introdues new problems and at rst it seems enough to onsider

only negation over atomi ations. We an have "positive" and "negative"

atomi ations. One ruial question is: Given an ation

a

^{, what does it}

meanbynegation of

a

^{? Doesitmeannotdoing}

a

^{,ordoinganything but}

a

^{? Do we wantto allowboth} interpretations? Ifso, we might need to have dierentnotations, like

a

^and

¬a

^{forthe two dierentnotions. Theintuitive}

meaningofanegativeation

a

^{is"notperforminga". Thatis,}

a

^isnotdened

as "the set of all the ations but

a

^{". One intrinsi problem onerning the}

denition of negative ationsis thatwhen performing anation,the urrent

statehanges,butwhatistheeetofnotperformanation? Isitnaturalto

onsider notperforminganationasbeinganationitself? Forexample,if I

withdrawmoney frommypersonal bank aount,then the aounthanges.

On the otherhand, ifI donotwithdrawany money,this negative ationhas

not eet on my bank aount. Though we do not have a onvining nal

solution on howto treat negation, we will see later the approah we take in

our ontrat language.

Besides, the above problem extends to obligation, permission and pro-

hibition over negative ations. For instane "you are not obliged to talk",

¬O(talk)

^{, might be} interpreted as "youhave the right toremain in silene"

(whih means "you have the right not to talk", i.e.,

P (talk)

^{). This shows}

that the intuitionof negated ationsonpermissionisin somesense dierent

from those on obligations, and it might be reasonable to allow them under

permissions.

2.5 On Obligation, Permission and Prohibition in E-

ontrats

Many of the researh ondutedby philosophersand logiianstend tostress

dierenes between ought and must, orto dene logial equivalenesbe-

tween obligation and permission, or even to fore one notion being dual of

ina philosophialontextorinpure logi,we laimthat wean avoidmany

of the above disussions given that we are restrited toeletroni ontrats.

In what follows we provide arguments for restriting syntatially the o-

urrene of ertainexpressions involvingobligation(

O

^{),permission(}

P

^{) and}

prohibition (

F

^{)in ae-ontrats.}

Inwhatfollowsweresumesomeoftheabovedisussions,andweintrodue

new insights of what should and should not be expressible in a ontrat

language.

•

^{Weonsiderstatementsexpressing oneisNOT obligedtodosomething}

is not intuitive inthe settingof e-ontrats.

¬O(a)

^{should not our in aontrat}

•

^{It is ounter intuitive to have iteration of ations under} obligation, permission and prohibition; e.g. it is not normal tohave in aontrat

a statement like: One is obliged to not pay, or pay one, o pay twie,

or

. . .

^.

O(a ^∗ )

^,

P (a ^∗ )

^{, or}

F (a ^∗ )

^{are not allowed}

•

^{AstatementlikeoneisNOTpermittedtodosomeation anberewrit-}

ten as one is forbidden to do the ation

¬P (a) ≡ F (a)

•

^{AstatementlikeoneisNOTforbiddentodoanation anberewritten}

as one is permitted to do the ation

¬F (a) ≡ P (a)

Notethatweadheretothelassialdenitionsofpermissionandprohibition

as one being the negationof the other.

We now disusssome restritions related toProhibition (

F

^).

•

^{It is not intuitive to have the}

+

^{under the}

F

^{operator. Consider for}

example the following norm: In Europe it is forbidden one of the fol-

lowing ations (but notboth): to driveon the left side of the road (

d l

^),

or todriveontherightside(

d _r

^{) whihanbe}representedas

F (d l +d r )

^.

The problemisthat itisnotlear underwhihirumstanes eahone

the hoie between two ationsis torelate eah of the ations with its

ontext. So, the above sentene ould be rewritten as: In the United

Kingdom it is forbidden to drive on the right side of the road. In the

rest of Europe (exept United Kingdom)it is forbidden to drive on the

left side of the road. Whih an beformalized as:

ϕ U K ⇒ F (d r ) ϕ REU ⇒ F (d l )

^.

Where

ϕ _{U K}

^and

ϕ _REU

^{are mutually exlusive. On the other hand, it}

is possible to forbid two ations

a

^and

b

simultaneously by imposing

F (a) ∧ F (b)

^.

Moreover, we argue that in ontrats it is not ommon to nd state-

ments that may be formalized using an exlusive OR operator

⊕

^be-

tween prohibitions. If we take the formula

F (a) ⊕ F (b)

^{to mean that}

either is forbidden

a

^{or forbidden}

b

^{but not forbidden both then one}

ase of the statement is

F (a) ∧ ¬F (b)

^{whih, using the above equiva-}

lene between

P

^and

¬F

^is

F (a) ∧ P (b)

^{. This means that one has the}

permission to do

b

^{. Similar from the seond ase, one may onlude}

that it ispermittedtodo

a

^{. In the end, the formula}

F (a) ⊕ F (b)

^does

notexpliitlyprohibitanything,makingitsuseompletelymeaningless

and dangerous.

•

^Theprohibitionofperforminganation

a

^{shouldimplythe}prohibition ofanyonurrentexeutionofanysetofationsthatontaintheation

a

^:

F (a) ⇒ F (a&b),

⁽²⁾

but the onverse impliationshould not hold:

F (a&b) 6⇒ F (a).

⁽³⁾

3 Puzzles and Paradoxes

Inwhatfollowswementionsomeofthemostimportantparadoxesofdeonti

logi (see forinstane [MN06℄for moredetails),and analyzeanew paradox

that arises in our approah.

Ross's Paradox [Ros41℄: In naturallanguageit isexpressed as:

1. It is obligatorythat one mailsthe letter.

2. It is obligatorythat one mailsthe letter or one burns the letter.

In Standard Deonti Logi (SDL) these are expressed as:

1.

O(p)

2.

O(p ∨ q)

The problem isthat in SDL one an infer that

O(p) ⇒ O(p ∨ q)

^.

The Good Samaritan Paradox [Pri58℄: In natural languagewe have:

1. It ought to be the ase that Jones helps Smith who has been

robbed.

2. It ought to bethe ase that Smith has been robbed.

And one naturally infersthat:

Jones helpsSmithwho has been robbed if and onlyifJones helps

Smith and Smithhas been robbed.

In SDL the rst two are expressed as:

1.

O(p ∧ q)

2.

O(q)

TheproblemisthatinSDLoneanderivethat

O(p∧q) ⇒ O(q)

^whih

is ounter intuitivein the natural language, asin the example above.

The Free Choie Permission Paradox [Ros41℄: Innaturallanguagewe

have:

1. Youmay either sleep onthe sofa or sleep onthe bed.

2. Youmay sleep onthe sofaand you may sleep onthe bed.

In SDL this is:

1.

P (p ∨ q)

2.

P (p) ∧ P (q)

The natural intuition tellsthat

P (p ∨ q) ⇒ P (p) ∧ P (q)

^{. In SDL this}

would lead to

P (p) ⇒ P (p ∨ q)

^{whih is}

P (p) ⇒ P (p) ∧ P (q)

^{, so}

P (p) ⇒ P (q)

^{. As anexample: If oneis permitted something, then one}

is permitted anything.

Sartre's Dilemma [MN06℄: In naturallanguage:

1. It is obligatorytomeet Jones now (aspromised to Jones).

2. It is obligatorytonot meet Jones now(as promised toSmith).

In SDL this is:

1.

O(p)

2.

O(¬p)

The problem is that in the natural language the two obligations are

intuitiveand oftenhappen, where thelogial formulas are inonsistent

when put together (in onjuntion) inSDL.

Chisholm's Paradox [Chi63℄: In naturallanguageit is expressed as:

1. John oughtto goto the party.

2. IfJohngoestotheparty thenhe ought totellthem he isoming.

3. If John does not go to the party then he ought not to tell them

he is oming.

4. John does not goto the party.

In Standard Deonti Logi (SDL) these are expressed as:

1.

O(p)

2.

O(p ⇒ q)

3.

¬p ⇒ O(¬q)

4.

¬p

The problem is that in SDL one an infer

O(q) ∧ O(¬q)

^{whih is due}

to statement (2).

The Gentle Murderer Paradox [For84℄: In natural language it is ex-

pressed as:

1. It is obligatorythat John does not kill hismother.

her gently.

3. John does killhis mother.

In Standard Deonti Logi (SDL) these are expressed as:

1.

O(¬p)

2.

p ⇒ O(q)

3.

p

The problemis that when adding a naturalinferene like

q ⇒ p

^then

in SDL one an infer that

O(p)

^.

3.2 A new paradox?

Apparently the deonti ommunity does not see, in general,

O(a) ∨ O(b)

as a problemati formula, but we believe it is indeed a problem to have

disjuntion of obligations and also of permissions and prohibitions. This

might be avoided in dierent ways depending on the approah, but in the

presene of onjuntion of ations and some of the usual relations between

obligation,permissionandprohibition,anewparadoxarises. Inwhatfollows

weexplainwhywethinktheaboveausesproblemsonthedeontireasoning.

Most of the approahes using logis for formalizing normative deonti

notions 5

propose anextension of propositionallogi (PL), meaning that the

logis inludeallthe tautologiesof PL.This naturallyinludesthe following

tautology:

A ⇒ A ∨ B

^{. We will show in what follows that from}

O(a)

^we

an derive

P (a) ∧ P (b)

^{whihislearlyadangerousparadox (ifIamobliged}

not totalk inthe presene of thePope,then I ampermittednot totalkand

to kill the Pope). In our derivation we use the followingommon relations:

• O(·) ⇒ P (·)

^,

• P (·) ≡ ¬F (·)

^.

We also make use of the De Morgan laws and the following intuitive

equivalenes:

• P (a&b) ≡ P (a) ∧ P (b)

^,

5

Usually thesenotionsareformalizedasoperatorsandin deontilogi areonsidered

tobemodalities. Thoughtheyarenotoperatorsinourapproah,wekeeptheterminology

whenevernoonfusionmightarise.

• F (a&b) ≡ F (a) ∧ F (b)

^.

Notie that the above is not standard sine many approahes do not

onsider onjuntionoverations,but itisveryintuitivetointerpretpermis-

sion and prohibition of onjuntion of ations as above. We are ready now

to showthat

O(a)

^implies

P (a) ∧ P (b)

^.

Firsttake

O(a) ⇒ O(a)∨O(b)

^{(instaneofthePLtautology}

A ⇒ A∨B

^).

From

O(a) ⇒ P (a)

^and

O(b) ⇒ P (b)

^{, we get that}

O(a) ∨ O(b) ⇒ P (a) ∨ P (b)

^{. But}

P (a) ∨P (b) ⇒ ¬F (a) ∨¬F (b)

^{andbytheDeMorganlawwehave}

that

¬(F (a) ∧ F (b))

^{whih implies}

¬F (a&b)

^{. We then get}

P (a&b)

^{whih is}

equivalent to

P (a) ∧ P (b)

^.

What is wrong on the above derivation? Some might argue that the

equivalenes given for permission and prohibition of ations are not univer-

sally aepted by the deonti ommunityand that they are not orret. We

believe that the ause of the problem relies on aepting ertain laws of

propositionallogiwhenreasoning aboutdeontimodalities(likede Morgan

laws). Moreover, we strongly advoate for the elimination of the lassial

disjuntion on normative deonti notions, given that the intuitive idea in

natural language when using the word or is usually that of an exlusive or

(Thelientisobligedtopayortosendanotiationof delay.,and another

example would be: Youhave the rightto remainsilentor anything you say

an be used against you in the ourt of law.). Thus, we laim that a logi

of ations(with onjuntion ofations)for aorret representation and rea-

soning of obligation, permission and prohibition should have the following

restritions:

•

^{The De Morgan laws annotbeapplied todeonti}modalities,

•

^{Use the exlusive or, and disallow} (syntatially)the lassial disjun- tion on deonti modalities.

Welaimthattherightinterpretationof

¬(O(a)∧O(b))

^shouldbe

¬O(a)∧

¬O(b)

^{, whih is more intuitive, in ase one admits the use of negationover}

obligations. Similarly forprohibition.

4 Desirable Properties of a Language for Con-

trats

Beforepresenting ourlanguagewestartbylistingsomeoftheintuitiveprop-

erties we should have, and others we should avoid, when formalizing on-

trats.

(a) Avoid the Good Samaritan paradox, Satre's dilemma, and the

GentleMurder paradox;

(b) Avoid Chisholm's paradox. This means obligation should be de-

ned onlyonations, not onformulas. In partiular donot write

formulas of the form

O(φ ⇒ ψ)

^;

() Avoid Ross's paradox. This means avoid having (in the lassial

notationof deontilogi):

O(p) ⇒ O(p ∨ q)

^;

(d) Avoid the Free Choie Permission paradox (i.e. do not allow the

following impliation:

P (p) ⇒ P (p ∨ q)

^);

(e) Avoidthe new paradox desribed inSetion3.2; i.e., syntatially

disallowthe lassialdisjuntion between deontimodalities.

(2) Use the XOR logialonnetive insteadof the lassialdisjuntionbe-

tween modalities;

(3) Allowonurrent ationsandkeepthe intuitionofonjuntiononobli-

gations; i.e.,

O(a&b) = O(a) ∧ O(b)

^.

(4) Some intuitive desirablerelationson obligations:

(a)

O(a; b) = O(a) ∧ [a]O(b)

(b) Allow CTD(reparation)

(5) Allowthedenitionofonditionalobligations,i.e.,formulasoftheform

ψ ⇒ O(a)

^.

(6) Have the following:

O(a) ⇒ P (a)

^.

(7) Do not dene permission and obligations in terms of eah other (for

instane, do not dene obligationas

O(a) = ¬P (¬a)

^).

(8) Some intuitive desirablerelationson permissions:

(a)

P (a; b) = P (a) ∧ [a]P (b)

(b)

P (a + b) = P (a) ⊕ P (b)

⁶

(9) Some intuitive desirablerelationson prohibitions:

(a)

F (a) = ¬P (a)

6

Manyauthorsprefertohave

P(a + b) = P(a) ∧ P (b)

^{(seeforinstane[BWM01℄).}

(b)

F (a; b) = F (a) ∨ haiF (b)

()

F (a + b) = F (a) ∧ f(b)

(d)

F (a) ⇒ F (a&b)

(e)

F (a&b) 6⇒ F (a)

(f) Allow ontrary-to-prohibition.

5 A Speiation Language for Contrats

This setionontains the denition of our speiation language for writing

e-ontrats. The rst two subsetions are meant as a tehnial preamble to

subsetion 5.3 where the language is dened. If the reader is more or less

familiarwiththeonept andtheintuitionofanation (fromdynamilogis

for example) then she may skip diretly tosubsetion 5.3. Subsetion 5.2is

intended to dene the onept of ation negation. This setion an also be

skipped ina rst reading.

5.1 Ation Algebra

Someofthemostwellknownandstudiedationalgebrasomefromthework

ondynamilogis [Pra76℄. We baseour workonPrattand Kozen'sdynami

algebra[Pra80, Koz80℄. This algebraisbuilt ontop of Kleenealgebrawhih

was introdued in 1956 and further developed by Conway in [Con71℄. For

referenes and anintrodutionto both Kleene and dynami algebra see the

extensive work of Kozen [Koz81, Koz90, Koz97℄.

Inthese researheorts the authorsused,for example,regularlanguages

as the objetsof the algebra, orrelationsover axed set (as wehave indy-

nami logi) and analyzed properties like ompleteness [Koz94℄, omplexity

[CKS96℄ and appliations [Coh94℄ of variants of Kleene algebra. Some vari-

ants inludethe test operator

?

^{, and others disardthe iterationoperator}

^∗

^.

Many insights an be drawn fromthis extensive work relatedto our need of

ation algebra.

We deneanalgebraistruture similartodynami algebra,modiedso

that it omplise with the intuition drawn from e-ontrats. A rst hange

is in dropping the Kleene star (iteration) as it isunnatural to have itunder

obligation,permissionand prohibitionoftheContratLanguage (seedisus-

sion in Setion 2.5). A seond hange involves the onurreny of two or

more ations,and itonsistsof dening aspeial operatorfor thealgebra to

model truly onurrent ations. For example, we need to express that The

lient is obliged to do ations a and b at the same time.

We reall that a Kleene algebra is a struture

K = {K, +, ·, 0, 1, ^∗ }

^with

the properties that

(K, +, 0)

^{is a ommutative monoid with the identity}

element

0

^,and

(K, ·, 1)

^{is a monoid with the identity element}

1

^{. Moreover,}

operator

+

^{is idempotent and thus it is possible to dene a partial order}

≤

on

K

^{thus having that}

(K, +, 0)

^{is a semilatie. The}

^∗

^{is a unary operator}

whihrespetsaset of axiomswith theintuitionthat

a ^∗ = 1 + a + a · a + . . .

^.

In programmingtheory itisusualtointerpret

+

^ashoie,

·

^{assequene and}

∗

as iteration.

A dynami algebra is a rather more omplex struture

D = (K, B, h·i)

where

K

^{is a Kleenealgebra,}

B

^{is a Boolean algebra, and}

h·i

^{a salar multi-}

pliationdened as

h·i : K × B → B

^{respeting the usual rules.}

Our ationalgebrahas aset of atomi ationsdenoted

A

^{and the ation}

operators whih form the ompound ations:

+

^{for hoie of two ations,}

·

^{for sequene of ations (or} onatenation; in PDL we nd this operator denoted as

;

^),

&

^{foronurrentexeutionoftwo atomiations,andthe test}

operator

?

^{(we will see later how with test operator we an simulate impli-}

ation over formulas [HKT00℄). The three operators

+

^,

·

^{, and}

&

^{are binary}

operators. Choie(

+

^{)isappliedtoompoundationsand isassoiativeand}

ommutative. Conurreny (

&

^{) operator is applied to atomi ations only}

and is assoiativeand ommutative. The sequene (

·

^{) operator isapplied to}

ompoundationsandisright-assoiativeandnon-ommutative. Forbrevity

we often drop the sequene operator and instead of

α · β

^{we just write}

αβ

^.

The operators

+

^,

·

^,and

&

^{are applied toelements of}

A

^(ations).

In dynami algebra, the elements of the boolean algebra are alled tests

and are inluded in the set of ations of the Kleene algebra (i.e. tests are

speial ations) 7

. Withthe test operatorthe

skip

^{ation (denoted}

1

^above)

isdenedas

⊤?

^,where

⊤

^{isthe speial}propositionthatholdsineveryworld.

1

^isinterpreted inPDL asthe identity relationoverthe set ofworlds. It has the meaning thatwhen exeutingthe

skip

^{atomiation the system goes to}

the samestate. With

skip

^theations

a

^and

a · 1

^{havethesame setoftraes,}

and

skip

^{has also the property that}

1 ^∗ = 1

^.

We do not study in this paper properties of this ation algebra but at a

rst look the

+

^and

·

^{operatorsobeythe same properties asthe operatorsof}

Kleene algebra. It is left to investigatethe properties of

&

^{operator and its}

relations with the other operators. Adding the test operator we obtain an

ation algebrawith tests [Koz97℄ and weexpet to have similar properties.

7

TobemoreformalandtohaveasyntaxmorelosertothesyntaxusedinPDLweuse

the

?

^{operator and allittest operator. Thetestoperatoris speialin thesense that it}

isappliedtoelementsof

B

^{(i.e. formulasinthebooleanalgebra)andgeneratesationsof}

A

^(i.e.

? : B → A

^{). Basially}

?

^{generatesthesetofationsalledtheset oftests inluded}

in

A

^.

It is known that for regular expressions there is no standard normal form;

for example, see the Starr-Height problem [Egg63℄ whih looks at regular

expressions normalforms fromthe perspetive of Kleene star.

For the set of ation operators (

+, ·, ^∗ , ?

^{) of the algebra dened in}

Setion 5.1 we have the following denition of ation normal form. For the

semantisofationsgivenwithtraes, asinproesslogis[Pra79℄,weobtain

all the traes of the ation.

Denition 5.1 (ation normal form for

+

^{). For ations dened with the}

operators

+, ·, ^∗ , ?

^{we have an ation normal form denoted by}

AN F ⁺

^and

dened as

α = +

ρ∈R ρ · α ^′

where

α

^{isa ompound ation,}

ρ

^{represents eitheran atomiation or atest,}

and

R

^{is a subset of atomi ations and tests.}

Theorem 5.1. For every ation in the algebra of Setion 5.1 we have a

orresponding

AN F ⁺

^.

Anaturalandusefulviewofationnegation whenweonsiderationsin-

terpretedastraesistosaythatthenegation

α

^ofation

α

^{istheationgiven}

by all the immediate traes that take us outside the trae of

α

^[BWM01℄.

With

AN F ⁺

^{it iseasy toformally dene}

α

^.

Denition 5.2 (ation negation). The ation negation is denoted by

α

^and

is dened for any ation

α

ⁱⁿ

AN F ⁺

^as:

α = +

ρ∈R ρ · α ^′ = +

b∈A\R b + +

ρ∈R ρ · α ^′

where

α ^′

^{is also in}

AN F ⁺

^{, and}

R

^{is a set of the atomi ations or tests.}

Note that

b

^{is only an atomi ation8 of}

A

^{, whih means that the ation}

negation doesnot takeintoonsiderationthe tests.

5.3 The Contrat Language

We aim at the denition of a preise syntax of a ontrat language, with a

translation into a logi in order to be able to reason about it. We dene

a Contrat Language (

CL

^{), and provide a set of rewriting rules in order to}

simplify and minimizethe numberof expressions in the language.

8

When we remove from the set of atomi ations

A

^{the set}

R

^{whih ontains both}

atomiationsandtests,theresultingsetwillontainonlytheationsof

A

^whiharenot

in

R

^.

language is:

Contract := D ; C

C := φ | C O | C p | C F | C ∧ C | [α]C | hαiC | C U C | C C _O := O(α) | C _O ⊕ C _O

C P := P (α) | C P ⊕ C P

C F := F (δ) | C F ∨ [δ]C F

Thesyntax of

CL

^{loselyresembles thesyntaxof amodal(deonti) logi.}

Though this similarity is learly intentional sine we are driven by a logi-

based approah,

CL

^{is not a logi. In what follows we provide an intuitive}

explanation of the

CL

^{syntax; a more preise meaning will be given later}

through atranslation into anextension of the propositional

µ

^-alulus.

A ontrat onsists of two parts: denitions (

D

^{) and lauses (}

C

^{). Note}

that we deliberately let the denitions part underspeied in the syntax

above.

D

^{speies the assertions (or onditions) and the atomi ations}

present in the lauses.

φ

^{ranges over Boolean} expressions inluding arith- meti omparisons, like the budget is more than 200$. For now we let the

atomi ations underspeied,whih for our purposes an beunderstoodas

onsisting of three parts: the proper ation, the subjet performing the a-

tion, and the target of (or, the objet reeiving) suh an ation. Note that,

in this way, the partners involved in aontrat are enoded in the ations.

C

^{is the general ontrat lause.}

C O

^,

C P

^{, and}

C F

^denote respetively obligation, permission, and prohibition lauses.

∧

^and

⊕

^{may be thought}

as the lassialonjuntion and exlusivedisjuntion, whihmay be used to

ombine obligations and permissions. For prohibition

C F

^{we have}

∨

^{, again}

with the lassial meaning of the orresponding operator.

α

^{is a ompound}

ationwithsyntaxasgiveninSetion5.1,while

δ

^{denotesaompoundation}

not ontaining any ourrene of

+

^. Operationally,we onsider that atomi ations do not require time for their exeution, i.e., the atomi ations are

instantaneous. Aonurrentationisalsoinstantaneous,soitanbeseenas

atomi. Note that syntatially

⊕

^{annot appear between} prohibitions and

+

^{annotour under}

F

^{, as wehave disussed in Setion2.5.}

WeborrowfromPDLthe syntax

[α]C

^{(alsoalleddynami box)torepre-}

sentthatafterperforming

α

^,

C

^{shouldbethease.} Intuitively,onemaythink of

[·]

^asthe

∀

^{quantierinthesensethateithertheationisnotperformedor}

if itisperformedthenthe lauseafteritshouldbeenfored. The

[·]

^notation

allows having a test inside, where the syntax

[φ?]C

^{must be understood as}

φ ⇒ C

^.

hαiC

^{(alsoknown asdynamidiamond)apturestheideathatthere}

(1)

O(α + β) = O(α) ⊕ O(β)

(2)

O(a&b) = O(a) ∧ O (b)

(3)

O(αβ) = O(α) ∧ [α]O(β)

(4)

P (α + β) = P (α) ⊕ P (β)

(5)

P (αβ) = P (α) ∧ hαiP (β)

(6)

F (αβ) = F (α) ∨ [α]F (β)

Table 1: Compositionalrules

must exist the possibility of exeuting

α

^{, in whih ase}

C

^{will be enfored}

afterwards. Intheontratlanguagewedonotrelatethe dynamiboxtothe

dynami diamond. They are related in

µ

^{-alulus, through their} translation of Setion 6.3. Following temporal logi (TL) [Pnu77 ℄ notation we have

U

(until)and

^{(next)withtheintuitivebehaviorasinTL.Thus}

C ₁ U C ₂

^states

that

C 1

^{should hold until}

C 2

^holds.

C

intuitively states that the

C

^should

hold in the next moment, usually after something happens. We an dene

C

^(always)and

♦ C

(eventually)forexpressing that

C

^{holdseverywhere and}

sometimes in the future, respetively.

The ompound ations have a ompositional behavior in

CL

^{when they}

appear under obligation

O

^{. Forhoie of ations we have}

O(α + β) = O(α) ⊕ O(β)

⁽⁴⁾

with the intuition(drawn fromthe world of ontrats) that If one is obliged

to hoose between doing oneation or doing another ation,then oneshould

regard it as being either obliged to do the rst ation or as being obliged to

do the seond ation.

Foronurrent ations we have

O(a&b) = O(a) ∧ O(b)

⁽⁵⁾

with the intuition that, regarding atomi ations If one is obliged to do an

atomi ation

a

^{and is also obliged to do another atomi ation}

b

^{then one}

should onludethat oneis obliged todo the two atomiations at the same

time.

Forthe sequene of ations wehave

O(αβ) = O(α) ∧ [α]O(β)

⁽⁶⁾

whihintuitivelymeansthatifoneisobligedtodoasequene ofationsthen

one should be obliged to dothe rst ation, and afterdoing the rst ation

one should alsobeobliged todo the seondation.

obligation. The hoie of ations is also exlusive hoie and we still have

ompositionallityof

P

^:

P (α + β) = P (α) ⊕ P (β)

⁽⁷⁾

whih intuitively means that if one is permitted to hoose between doing

one of the ations

α

^or

β

^{then, one is either permitted the rst ation or is}

permittedthe seond ation.

For onurreny under permission we do not nd any ompositionallity

rule. A lause

P (a&b)

^{stating that it is permitted to do the two ations at}

the same time, does not give any information about the individual ations.

Moreover, the permission of the individual ations an not give information

about the permissionof the onurrent exeutionof the two ations.

Forthe sequene of ations underpermissionwe have:

P (αβ) = P (α) ∧ hαiP (β)

⁽⁸⁾

with the intuitionthatif oneis permittedtodothe sequene of ationsthen

one may onlude that one is both permittedthe rst ationand alsothere

exists a way ofdoing therst ationand afterwords onewould be permitted

the seondation.

Compound ations under prohibition do not behave the same as under

obligation orpermission. For onurreny under prohibition we donot nd

any ompositionallity rule; (see equations(2), and (3)of Setion2.5).

Forthe sequene of ations underprohibition we have

F (αβ) = F (α) ∨ [α]F (β)

⁽⁹⁾

with the intuitionthat if one isforbiddento dothe sequene of ationsthen

one may onlude that one is eitherforbidden the rst ation or,if the rst

ation is performed the seondation is forbidden.

The main dierene between modal logi (where the modality denotes

neessity) anddeontilogi(where themodalitydenotesobligation)isinthe

fat that the deonti modality an be violated. For example, if in modal

logi one an make the inferene:

p

^then

p

^{(if it is neessary that}

p

^{, then}

p

^{is true), in deontilogi the inferene is nolonger possible beause}

O

^an

be violated (see Setion 2.1 for a disussion). Relatedto this we onstantly

nd in ontrats the ontrary to duty (CTD) and ontrary to prohibition

(CTP)formulas. CTDs expresswhat happens ifanobligationisviolated. In

our ase, if we have the obligationto do an ation then the violation of the

obligationisthe exeutionof the negationof the ation. CTDs are added to

the ontrat language withthe following syntax:

O ϕ (α)

stating the obligationtoexeute the ompoundation

α

^{and the reparation}

formula

ϕ

^{whihshouldholdinasetheobligationisviolated. Thereparation}

may be either another obligation,a prohibition, a stand alone assertion, or

even another CTD whih should beenfored afterthe violation ours. The

above is syntati sugar for the following

CL

^formula:

O ϕ (α) = O(α) ∧ [α]ϕ

⁽¹⁰⁾

stating the obligation

O(α)

^{whih should hold in the urrent world and if}

the negation of

α

^{is exeuted (meaning that the obligation is violated) the}

reparation

ϕ

^{shouldbeenfored.}

One might suggest that just the ation negation as dened in Setion

5.2 does not apture the intuitionof violation of anobligation of anation.

One may say that for an ation

a

^{(e.g. deposit money in the bank aount)}

a violating ation may be just the negative ation

¬a

^{(NOT deposit money}

in the bank aount). In this paperwe do not onsider negativeations; for

a disussion about our deision see Setion 2.4.3. A seond argument for

our deision is that negative ations may be expressed in other ways. For

example, inorder to say obliged NOT to do one an say forbidden to do.

Contrary toProhibitionstatements expliitlyprovide the reparationfor-

mulawhihshouldholdinasetheprohibitionisviolated. Forexampleifthe

forbidden ation

α

^{isexeuted (the} prohibition isviolated) then a reparation formula

ϕ

^{should be enfored. The CTPs (denoted as}

F ϕ (α)

^{) are abbrevia-}

tions of the

CL

^formulas:

F _ϕ (α) = F (α) ∧ [α]ϕ

⁽¹¹⁾

Withthedynamiboxsyntaxweanmodelin

CL

^onditionalobligations, permissions, and prohibitions(see Dyadi Deonti Logi for an introdution

to the formalism that has introdued onditional obligations [PS97℄). We

may have two kinds of onditional expressions; let us take an example for

obligation. Conditional obligations an depend on both the exeution of

an ation, or on an assertion whih holds in the urrent state. Intuitively,

onditionalobligationsrelatedtoationsstatethatafterexeutinganation,

a ertainobligationisthe ase. We represent suh onditionalobligationas:

[α]O(β)

⁽¹²⁾

where

α

^{is the} onditioning ation and

O (β)

^{is the obligation enfored by}

the onditioning ation. Often in ontrats we nd obligationstriggered by

some assertion that holds in the urrent world. Intuitively, if the assertion