# coco_runtime_reasoning_about_conflicting_commitments__bfc9a8e0.pdf

Coco: Runtime Reasoning About Conﬂicting Commitments

Nirav Ajmeri, Jiaming Jiang, Rada Chirkova, Jon Doyle, Munindar P. Singh

North Carolina State University, Raleigh, NC 27695, USA {najmeri, jjiang13, rychirko, Jon Doyle, singh}@ncsu.edu

To interact effectively, agents must enter into commitments. What should an agent do when these commitments conﬂict? We describe Coco, an approach for reasoning about which speciﬁc commitments apply to speciﬁc parties in light of general types of commitments, speciﬁc circumstances, and dominance relations among speciﬁc commitments. Coco adapts answer-set programming to identify a maximal set of nondominated commitments. It provides a modeling language and tool geared to support practical applications.

1 Introduction

Major applications of information technology presuppose an ability to reason about interactions among autonomous parties. We characterize the expectations that parties have of one another using a notion of commitment in which general commitment schemata produce speciﬁc commitment instances when applied to speciﬁc parties in speciﬁc situations. In some situations, commitment instances demand conﬂicting conditions or assignments of resources. We characterize the means for resolving such conﬂicts in terms of situation-dependent dominance relations among commitments.

Example 1. Alice, a child, takes ill. Society expects Alice s guardian, Bob, to take her immediately to her pediatrician, Carol, provided Alice requires immediate medical attention. Meanwhile, Bob s employer, Steve, expects him to work during business hours. Bob disregards his employer s expectation in light of the medical emergency involving his ward.

Following Singh [2013], we use the term principal to mean an autonomous party (person, agent, organization, or polity) that can commit to others and be committed to by others. Example 1 includes as principals the people named and Society.

Bob is committed to Steve to stay at work during work hours, and to Society to take Alice to Carol if Alice becomes sick. If someday Alice falls sick during work hours, instances of the above schemata arising on that day conﬂict because Bob cannot be at two places at once. If that is all we know, there is no clear resolution. But the resolution is clear if it is more important for Bob to bring Alice to Carol when she is sick than to go to work.

Problem. The problem we address is how to resolve commitment conﬂicts that are resolvable through runtime reasoning about situation-dependent dominance among instances.

Novelty. Commitments, norms, and compliance have been extensively studied. Yet, despite many advances, previous work has not tackled the stated problem. Most treatments of commitments and norms do not represent dominance. Yolum and Singh [2004] and Alberti et al. [2006] compute feasible execution paths for agents or verify compliance. Dignum et al. [2005] deﬁne a CTL variant and present a formalism of deadlines to determine norm compliance based on whether agents bring about speciﬁed states before the deadline. Alechina et al. [2013] (hereinafter, ADL) apply CTL and ATL to reason about normative update. They incorporate deadlines and determine compliance via a notion similar to Dignum et al. s. ADL s framework sanctions violators. Although Dignum et al. and ADL consider time, they do not consider dominance between norms. Knobbout and Dastani [2012] propose a logical framework by extending ATL to reason about agents abilities under norm-compliance assumptions, but lack a notion of dominance.

Vasconcelos et al. [2009] and Governatori [2007] address conﬂicts between norms as a design problem with a view to specifying schemata (in our terminology) that avoid potential conﬂicts. In contrast, Coco aims to resolve conﬂicts as they arise between instances. This has the beneﬁt of only having to deal with conﬂicts that occur, not those that might occur. The contrary-to-duty literature, e.g., [Prakken and Sergot, 1996], deals with secondary obligations that come into effect when the primary obligations are violated.

Boella and van der Torre [2008] provide a mechanism for expressing which norm supersedes which other in which situation, but their work does not address automatic runtime identiﬁcation of nonsuperceded instances.

Some heuristic approaches are promising. Oren et al. [2008] propose an argumentation-based heuristic to determine which norms to comply with when norms conﬂict. They build conﬂict graphs with norms and conﬂicts as nodes and edges. Oren et al. use agent preferences to prune norms in conﬂict graphs, and permanently drop nonpreferred norms. Oren et al. s work ignores temporal aspects. In contrast, Coco deals with commitments at runtime.

Criado et al. [2015] propose an economics-based approach

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

that resolves conﬂicts among instances of norms by optimization using agent objectives and preferences. The optimization function, built into the conﬂict-resolution algorithm, considers the coherence of the available cognitive and normative elements. In contrast, Coco uses explicit rules to specify dominance among commitment instances. These rules enable tracing and interpretation of conﬂict resolutions in terms of agent objectives and preferences.

Contributions. Coco provides representations for commitments and dominance, as well as tractable decision procedures for determining compliance of actions with commitment instances. Coco (1) applies answer-set programming (ASP) [Gelfond, 2008; Gebser et al., 2014] to identify nondominated commitments given knowledge of the world and of the speciﬁc situation, and (2) applies ADL s techniques to determine compliance of agent actions with nondominated commitment instances. This paper also provides theoretical results on the correctness and tractability of the problems of (3) determining maximal sets of nondominated commitment instances, and (4) determining liveness and safety of a system of commitments.

2 Specifying Commitments

A commitment here involves two principals, with the creditor principal committed in some way to the debtor principal. A commitment schema (dbt, crd, φ, , td) indicates that debtor dbt is committed to creditor crd so that if the antecedent condition φ holds, then the consequent condition should hold at some point within the deadline duration td, meaning that should hold at some time within time units after φ begins to hold.

We write (s, dbt I, crd I, ti) to mean a commitment instance in which s is the commitment schema that the instance instantiates, dbt I and crd I are the speciﬁc debtor and creditor (i.e., the principals who ﬁll the corresponding roles in the schema), and ti is the time at which the instance becomes detached, i.e., at which the schema s antecedent for the particular debtor and creditor becomes true.

Listing 1 formalizes a commitment schema, g Com, committing guardians to take care of their charges, as open (implicitly universally quantiﬁed) FOL formulas. We use capitalized words to represent variables, and lowercase for constants. Statements 2 and 3 mean that if G ﬁlls the guardian role for charge C at T, then G is the debtor of the g Com instance, and C is the creditor. Statements 4 and 5 state the antecedent and consequent, respectively. The antecedent is that C falls sick, and the consequent is that G brings C to C s pediatrician Ped. Line 6 states that the deadline duration is 3 time units.

Similarly, the schema w Com deﬁned in Listing 2 commits employees to be at work during work hours. If employee Ee s employer is Er at time T, then Ee is the debtor and Er is the creditor of the w Com instance. The antecedent of w Com is that time T is a work hour for employee Ee at employer Er, and the consequent is Ee is at work for Er at time T. The deadline duration is 0 time units.

1 schema(g Com) 2 guardian R(C, G, T) ! dbt(g Com, G, T) 3 guardian R(C, G, T) ! crd(g Com, C, T) 4 [sick(C, T) crd(g Com, C, T)] ! ant(g Com, T) 5 [bring(G, C, Ped, T) ped R(C, Ped, T)

dbt(g Com, G, T) crd(g Com, C, T)] ! con(g Com, T) 6 d Duration(g Com, 3)

Listing 1: Deﬁnition of the g Com schema

1 schema(w Com) 2 employer(Ee, Er, T) ! dbt(w Com, Ee, T) 3 guardian R(C, G, T) ! crd(w Com, Er, T) 4 [dbt(g Com, Ee, T) crd(w Com, Er, T)

workhour(Ee, Er, T)] ! ant(w Com, T) 5 [dbt(w Com, Ee, T) crd(w Com, Er, T)

at Work(Ee, Er, T)] ! con(w Com, T) 6 d Duration(w Com, 0)

Listing 2: Deﬁnition of the w Com schema

We treat compliance and conﬂict with respect to instances. Thus, if Alice falls sick at time instant T, an instance of g Com is instantiated and becomes detached at T. If Bob takes Alice to her pediatrician within three hours, then the instance is satisﬁed. Otherwise, the instance is violated.

3 Formal Language and Model Coco s formal language is the function-free ﬁrst-order predicate calculus with a distinguished set of predicates and constants. To describe facts of the world, it contains (1) constants naming all principals in lowercase, such as alice and bob, distinguished times, such as time 10, within a ﬁnite interval, and durations; (2) predicates naming roles of organizations, such as guardian R, indicated by names ending in R; (3) predicates naming conditions of interest, such as workhour; (4) predicates naming actions, such as bring; and (5) predicates < (precedes), = (equals), and (precedes or equals) for comparing times.

To describe commitments, the language contains (1) constants naming schemata; and (2) terms naming instances of schemata. For example, the ground term instance(g Com, bob, alice, 10), which we abbreviate to g Com Inst in the following, names an instance of g Com with debtor bob and creditor alice detached at time 10. Similarly, the term instance(w Com, bob, steve, 11), abbreviated henceforth as w Com Inst, names an instance of w Com.

The methods described in Section 4.2 for testing liveness and safety require a function-free language. When forming instances, Coco asserts statements that identify the components of an instance term, as illustrated for g Com Inst in Listing 3.

1 [s Inst(g Com Inst) is Inst Of (g Com Inst, g Com)]

! crd I (g Com Inst, alice) 2 [s Inst(g Com Inst) is Inst Of (g Com Inst, g Com)]

! dbt I (g Com Inst, bob) 3 d Duration I (g Com Inst, 3)

Listing 3: Some properties of g Com Inst

The antecedent and consequent of an instance, omitted in the listing, are formed by substituting the names of speciﬁc debtor and creditor for the corresponding variables in the schema.

Table 1 lists the main predicates of schemata and instances of Coco. S is a refers to a schema, and Si refers to an instance. schema and s Inst specify the corresponding types; is Inst Of identiﬁes the schema of an instance; and ant I and con I state that instance antecedents and consequents hold at speciﬁc times.

Schema predicates

schema(S) dbt(S, P, T) crd(S, P, T)

ant(S, T) con(S, T) d Duration(S, T) Instance predicates

s Inst(Si) is Inst Of (Si, S) dbt I (Si, P) crd I (Si, P) ant I (Si, T) con I (Si, T) d Duration I (Si, T) detached(Si, T) same Dbt I same Crd I

violated(Si, T) satisﬁed(Si, T) becomes Detached(Si, T) becomes Violated(Si, T) becomes Sat(Si, T) conﬂicting(Si1, Si2, T) dominates(Si1, Si2, T) dominated(Si, T) con INot Hold(Si, T1, T)

Table 1: Main predicates of schemata and instances.

The satisfaction of an instance is formalized as becomes Sat(Si, T), which means that T is the ﬁrst time at which the consequent of Si holds, provided this happens before the deadline; satisﬁed is true of the instance from that time on. The violation of an instance is realized in a similar way. Speciﬁcally, the statement becomes Violated(Si, T) holds at T when Si is detached, but not dominated, and its consequent does not hold within the deadline. The definitions for becomes Sat and becomes Violated are provided in Listing 4. The predicate con INot Hold(Si, T1, T) says that the consequent of Si is not true between times T1 and T. The two utility predicates di erence(T1, T2, T) and addition(T1, T2, T 0) state that the difference and sum of T1 and T2 are T and T 0, respectively.

1 [detached(Si, T 0) con I (Si, T) di erence(T, T 0, 1)]

! becomes Sat(Si, T) 2 [becomes Detached(Si, T1) d Duration I (Si, T2)

addition(T1, T2, T) con INot Hold(Si, T1, T) dominated(Si, T)] ! becomes Violated(Si, T) Listing 4: Satisfaction and violation relations

We deﬁne a set of instances as conﬂicting if the set of their consequents cannot hold simultaneously. Whether a consequent can be true when another consequent is true depends on the domain knowledge of speciﬁc scenarios. Section 5 formalizes knowledge showing how g Com Inst and w Com Inst conﬂict in our example. Listing 5 deﬁnes conﬂicting(Si1, Si2, T) symmetrically as holding at time T in case Si1 and Si2 are detached but their consequents cannot both hold at T.

1 [detached(Si1, T) detached(Si2, T)

(con I (Si1, T) $ con I (Si2, T))] ! conﬂicting(Si1, Si2, T)

Listing 5: The conﬂicting relation

In Example 1, Bob is required to be at his workplace during work hours and at Carol s ofﬁce with Alice when Alice is sick. If Alice gets sick during Bob s work hours, both g Com Inst and w Com Inst detach and require Bob to be in two places at the same time. The consequent conditions conﬂict even when Alice is not sick, but only matter for detached instances; only then may such conﬂicts cause a commitment violation.

We resolve such conﬂicts by employing dominance relations, so that satisfaction of a more dominant instance vitiates violation of a less dominant instance. Thus, a principal can comply with one instance while violating another, and still remain in compliance with the entire set of instances. We require that the relation dominates (more dominant than) be a strict partial order, that is, transitive and irreﬂexive. A partial order is appropriate because changing commitments and unforeseen conﬂicts may make a total ordering infeasible; a partial order can sufﬁce to resolve conﬂicts that do arise. We select from the set of all detached instances a maximal subset of nondominated instances, that is, a subset of detached instances none of which is less dominant than some conﬂicting instance in the same set.

Listing 6 formalizes simple dominance of g Com over w Com. The statement says that a detached instance of g Com dominates a detached instance of w Com if they have the same debtor and the same creditor, which are indicated by the utility predicates same Dbt I and same Crd I . Section 5.2 gives examples in which this dominance is narrowed by requiring additional conditions.

1 [is Inst Of (Si1, g Com) is Inst Of (Si2, w Com)

detached(Si1, T) detached(Si2, T) same Dbt I (Si1, Si2) same Crd I (Si1, Si2)] ! dominates(Si1, Si2, T) Listing 6: The guardian dominance relation

Listing 7 deﬁnes dominated(Si1, T) to hold at T in case a detached instance Si1 is in conﬂict with another detached, nondominated instance Si2 that dominates it at T.

1 [dominates(Si2, Si1, T) conﬂicting(Si1, Si2, T)

dominated(Si2, T) detached(Si1, T) detached(Si2, T)] ! dominated(Si1, T)

Listing 7: The dominated relation

4 Decision Procedures, Theoretical Results

Given a Coco snapshot of the current enactment, speciﬁcally the current state of the knowledge on the detached instances and the appropriate background knowledge, we test whether the snapshot admits an unambiguous nondominated set of currently detached instances, which we call a nondominated set. If it does, we obtain a maximal such set, D, and then proceed to check the liveness and safety properties of D.

In Ex. 1, the set D would contain (i) a nondominated instance for Bob taking Alice to the hospital, and (ii) a dominated instance for Bob having to be at work at the same time.

4.1 Testing for Existence of Nondominated Set We test enactments for admission of nondominated sets of detached instances by obtaining stable models under ASP semantics, e.g., [Gelfond, 2008], and by interpreting the outputs in our setting. Intuitively, we take a snapshot S as input, and return a stable model of S under ASP semantics, that is, all the facts implied by S under the semantics that do not become negated under inferences using the rules of S.

Deﬁnition 1. For a noncontradictory snapshot S of knowledge about an enactment, we call a set D of detached instances in S a nondominated set of detached instances whenever for each instance nii in D, the following holds:

(a) It is not possible to infer (under ASP) from S the fact

dominates(nij, nii, t) for any detached instance nij in S and time t at which nii and nij are in conﬂict; and

(b) It is not possible to infer from S the fact that nii conﬂicts

with any other detached instance in D at time t.

We call any such set D saturated if it includes each detached instance in S that satisﬁes condition (a) above.

The intuition for saturated sets of detached instances is that each such set witnesses that for each pair in S of detached instances nii and nij that are in conﬂict at time t, S entails the fact of dominance at time t of either nii by nij or vice versa. That is, our dominance knowledge is complete in this case for all the detached instances in snapshot S.

Given a snapshot S, with each stable model M of S we associate the M-nondominated set of detached instances in S, written D(S, M), as follows: D(S, M) is a maximal set of detached instances nii 2 S such that

(1) M does not include the fact dominates(nij, nii, t) for

any detached instance nij in S at time t, and

(2) It is not possible to infer from S the fact that nii conﬂicts

with any other detached instance in D(S, M).

The set D(S, M) may or may not be saturated, depending on the degree of completeness of the dominance knowledge that can be inferred from the snapshot S. (For example, if S entails the fact of conﬂict of two instances, nii and nij, but does not entail any dominance knowledge, then two sets D(S, M) = {nii} and D(S, M0) = {nij} may exist, with neither set being saturated or saturable.)

We further say that two stable models M and M0 of S are nondominance identical if and only if their associated sets D(S, M) and D(S, M0) are the same.

Theorem 1. Given a noncontradictory snapshot S: At least one stable model for S exists and is nondominance identical to all stable models for S if and only if there exists for S a saturated nondominated set of detached instances in S.

For instance, in Example 1 there exists a single stable model with instances (i) and (ii) as in the beginning of this section, provided S captures that g Com dominates w Com when Alice is sick. Otherwise, ASP would compute two or

more stable models, an indication that S does not admit a saturated nondominated set of detached instances in S.

Proof. (sketch) We begin by proving the existence claim of Theorem 1. The only if part is immediate from the deﬁnitions.

For the if part, suppose that there exists for S a saturated nondominated set, D, of detached instances in S. We show that in this case there exists at least one stable model, M, for the snapshot S, such that D is the D(S, M) associated with M. Indeed, by deﬁnition of D, for each element nii of D one cannot infer from S that nii is in conﬂict with another detached instance that dominates it. Further, D includes all the instances in S that satisfy the condition (a) in Deﬁnition 1. Thus, D is a unique and maximal set w.r.t. the detached instances entailed from S. We now obtain the set J of all the facts implied from S; the set M = S [ J is a stable model of S by construction. It is immediate from the deﬁnitions that D is the set D(S, M).

We now prove by contradiction that under the assumptions of the previous paragraph, all the stable models of the given snapshot S are nondominance identical. Indeed, assume there exists a stable model, M0, of the snapshot S, such that the set D(S, M0) is not identical to the saturated set D as deﬁned above. By deﬁnition of D, the only way this can happen is when D(S, M0) is a proper subset of D. (Recall that the snapshot S is noncontradictory.) This means that for at least one detached instance nii 2 S, such that nii /2 D(S, M0), one cannot derive from S that nii is dominated by another detached instance nij 2 S, at time instant t. At the same time, nii is not in conﬂict with any element of D(S, M0), as witnessed by the existence of the set D. It follows that the set D(S, M0) is not maximal as required by deﬁnition of associated set for M0, a contradiction.

Theorem 2 is immediate from Theorem 1.

Theorem 2. Given a noncontradictory snapshot S: The asymptotic runtime complexity of (a) determining whether a saturated nondominated set of detached instances in S exists and (in case it exists) of (b) producing such a set coincides with the runtime complexity of ﬁnding the stable models of S.

4.2 Liveness and Safety Checking Suppose that for a snapshot S, there exists a saturated nondominated set D of detached instances in S. Then it follows from Theorems 1 and 2 that it is decidable and tractable to construct D using a standard ASP solver. Suppose that we further want to check whether certain liveness and safety properties hold in S in presence of D.

Following ADL, we understand liveness as capturing that desirable states (from the designer s point of view) are possible w.r.t. the current enactment and can be achieved without an agent incurring sanctions, and safety as capturing that it is impossible for an agent to reach a state where some undesirable property holds without incurring some sanctions. Our approach for checking liveness and safety properties is by reduction to ADL s approach, as follows.

Given a liveness or safety property, ', in the context of a snapshot S and of its nondominated set D, we translate each of ', S, and D into propositions by using separate proposition

names for all possible instantiations of the predicates in ', S, and D with the constants in the given universe of discourse. (We assume there is a constant upper bound on the arity of the predicates and rules in S, ', and D. That is, we do not consider the arity of the facts or rules in S, ', or D a variable part of the input.) We then treat the result of this process, S2, as an input to ADL s approach, and treat the output of the latter approach as follows.

Theorem 3. Let S2 be a knowledge base as described above and including a suitable transformation of a liveness or safety property, ', on a snapshot S that admits a saturated nondominated set D. Then ADL s algorithm [2013, proof of their Theorem 1], when given S2 as its input, outputs the answer yes (respectively, no ) if and only if the property ' holds (respectively, does not hold) on S in presence of D.

Proof. ADL express liveness and safety properties in CTLS, a sanctions-based extension of CTL [Clarke et al., 1986]. ADL check a liveness or safety property ' against a set N of conditional norms and a transition system M via model checking. (Due to the page limit, we refer the reader to Alechina et al. [2013] for the details.) Model checking takes as inputs a transition system M with initial state s, a ﬁnite set of conditional norms N, and a formula ' of CTLS. It returns true if M N, s |= , and returns false otherwise. Here, M N is a normative update of M with N, with the meaning of an expansion of M into all possible complete paths (runs) and with all the norms in N enforced on all the runs.

It is straightforward to verify that (1) the transformation of S, ', and D into S2 described above results in S2 that is a correct propositional expansion of the inputs, and of size bounded by a polynomial in the size of the inputs, and that (2) the result S2 of the translation constitutes a valid input to ADL s checkers. As a result, ADL s checkers provide correct answers for S, ', and D via providing correct answers for S2 and via S2 being their correct propositional expansion.

By the results of Alechina et al. [2013], the modelchecking problem for a normative update of a transition system is PSPACE complete; the proofs are constructive and thus provide a PSPACE-complete algorithm for verifying whether a given liveness or safety property holds against a set of conditional norms and a transition system.

Consequently, checking liveness and safety properties of enactments that admit saturated nondominated sets of instances is decidable with asymptotic runtime complexity of PSPACE, equal to that of ADL s approach.

5 Demonstration

We now demonstrate the Coco workﬂow and formalize conﬂict detection using Example 1. We then show how to add constraints to dominance relations in Section 5.2.

5.1 Formalizing the Example Figure 1 illustrates Example 1, omitting time instants before 10 and after 13 for brevity. Each node represents the state update of an instance. One time instant contains multiple nodes if there are state updates of multiple instances at that

time. The line above a node is the debtor s action, represented as a predicate, that caused the state update. For example, Alice becomes sick at time 10, which causes detachment of g Com Inst. Then at time 11, the middle node (labeled 11) indicates detachment of w Com Inst. Node 11b says w Com Inst becomes satisﬁed if Bob is at work at 11. Similarly, 11a says g Com Inst becomes satisﬁed if Bob brings Alice to her pediatrician at time 11. A conﬂict occurs at time 11 because Bob cannot be at two places at once, assuming Carol s ofﬁce is at hospital Loc, Bob s work is at company Loc, and the two are distinct. Finally, node 13 indicates that with the conﬂict detection and dominance relation, g Com Inst would not become violated even if Bob did not bring about the consequent.

workhour (bob, steve, 11)

bring (bob, alice, carol, 11) at Work (bob, steve,11)

sick(alice, 10)

becomes Detached( instance(w Com (bob,steve,11),11)

becomes Sat( instance(w Com (bob,steve,11),11)

becomes Sat( instance(g Com (bob,alice,10),11)

becomes Detached( instance(g Com (bob,alice,10),10)

becomes Violated( instance( g Com (bob,alice,10),13)

dominates( instance(w Com (bob,steve,11),11)

dominates conflicts

Figure 1: A healthcare scenario (see Example 1)

In summary, Coco ﬁnds that g Com Inst dominates w Com Inst at time 11; g Com Inst is satisﬁed at 11 (when Bob brings Alice to Carol). The execution demonstrates how, in the presence of dominance relations, an enactment can comply with a set of instances without complying with each of them.

Consider the scenario where, instead of bringing Alice to the hospital when she is sick, Bob chooses to work, illustrated in Figure 1 by the path 10!11b!12b!13b. Coco produces an output similar to the previous case but ﬁnds that g Com Inst is violated at time 13 and w Com Inst is satisﬁed at 11. The nondominated instances remain violated if their consequents do not hold within the deadline, whereas a dominated instance may be satisﬁed.

Listing 8 formalizes the conﬂict detection for this enactment. Statement 1 says the same principal cannot be at two different locations at the same time. Statements 2 4 imply that w Com Inst s consequent cannot be true at T when

g Com Inst s consequent holds at T. Lines 5 7 handle the converse. Thus, g Com Inst and w Com Inst instances conﬂict and the latter is dominated.

1 [at Location(P, L1, T) (L1 6= L2)]

! at Location(P, L2, T)

2 [is Inst Of (Si, g Com) con I (Si, T) dbt I (Si, G)]

! at Location(G, hospital Loc, T) 3 [employer R(Ee, Er, T)

at Location(Ee, company Loc, T)] ! at Work(Ee, Er, T) 4 [is Inst Of (Si, w Com) dbt I (Si, Ee) crd I (Si, Er)

at Work(Ee, Er, T)] ! con I (Si, T)

5 [is Inst Of (Si, w Com) con I (Si, T) dbt I (Si, Ee)

crd I (Si, Er)] ! at Location(Ee, company, T) 6 [guardian R(C, G, T) ped R(C, Ped, T)

at Location(G, hospital Loc, T)] ! bring(G, C, Ped, T) 7 [is Inst Of (Si, g Com) dbt I (Si, G) crd I (Si, C)

ped R(C, Ped, T) bring(G, C, Ped, T)] ! con I (Si, T) Listing 8: Conﬂict-detection knowledge for Example 1

5.2 Additional Dominance Relations Dominance relations can be speciﬁed incrementally to cover conﬂicts between different types of commitments in different circumstances. For example, suppose Bob s wife, Amy, is also available and responsible for Alice, and consider the following modiﬁed scenario. Example 2. Alice, Bob and Amy are all at home and Bob needs to go to work. Alice suddenly takes ill and Bob would be late for work if he takes Alice to her pediatrician. Meanwhile, Amy is taking a day off and available for taking care of Alice. So Bob goes to work and Amy immediately takes Alice to the hospital.

Formalizing Example 2 involves another instance of g Com, namely instance(g Com, amy, alice, 10), abbreviated g Com Inst2. We want g Com Inst2 to dominate g Com Inst because Amy is currently available but Bob is not. We formalize this availability-dependent dominance relation in Listing 9. Speciﬁcally, a detached instance Si1 of g Com dominates another detached instance Si2 of g Com if they have the same creditor, Alice in this case, but different debtors, Bob and Amy in this case, and Si1 s debtor is available while Si2 s is not.

1 [is Inst Of (Si1, g Com) is Inst Of (Si2, g Com)

detached(Si1, T) detached(Si2, T) same Crd I (Si1, Si2) dbt I (Si1, G1) dbt I (Si2, G2) (G1 6= G2) available(G1, T) available(G2, T)] ! dominates(Si1, Si2, T) Listing 9: The availability dominance relation

In Example 2, g Com Inst2 is nondominated. However, g Com Inst2 dominates and conﬂicts with g Com Inst, so g Com Inst is dominated. As before, g Com Inst dominates w Com Inst, so by transitivity, g Com Inst2 dominates

w Com Inst. Although g Com Inst still conﬂicts with w Com Inst, w Com Inst is nondominated because g Com Inst is dominated and because it does not conﬂict with g Com Inst2.

Consider the situation where neither Bob nor Amy is available, then we could augment the dominance relation given in Listing 9 to say that whoever is closer to Alice should take her to the hospital. Listing 10 formalizes this using the dist(G,C,D,T) predicate to say the distance between G and C at time T is D.

1 [is Inst Of (Si1, g Com) is Inst Of (Si2, g Com)

detached(Si1, T) detached(Si2, T) same Crd I (Si1, Si2) crd I (Si1, C) dbt I (Si1, G1) dbt I (Si2, G2) (G1 6= G2) available(G1, T) available(G2, T) dist(G1, C, D1, T) dist(G2, C, D2, T) (D1 D2)] ! dominates(Si1, Si2, T) Listing 10: Distance Dominance Relation

6 Discussion Coco provides a ﬂexible formalization of instances, including reasoning about conﬂicts and dominance. It employs ASP to compute maximal consistent sets of instances and adapts ADL s techniques to tackle compliance, liveness, and safety. Coco supports identifying and dealing with conﬂicts between commitments arising at runtime.

Additional related work. Besides the works discussed in Section 1, works on policy reasoning and software engineering are relevant. Marinovic et al. [2014] formalize breakglass reasoning in which a user can override access control based on urgency but thereby becomes subject to additional monitoring (e.g., CCTV) and post facto justiﬁcation requirements. Marinovic et al. adopt multivalued reasoning to determine a suitable decision for the access control system.

Ingolfo et al. [2014] propose N omos 3, a goal-based framework to determine compliance of roles and requirements. They consider two norms (rights and duties) and propose two roles (social and legal). When a social role has to achieve a goal, the corresponding legal role must be compliant, i.e., it has to satisfy required preconditions and postconditions of norms. Their distinction of roles is not substantial. Ingolfo et al. provide a graphical modeling language for compliance, but it is limited and does not support deﬁning dominance among norms. Ghanavati et al. [2014] provide heuristics for reading textual regulations to determine their meanings and potential dominance relations. They do not deal with instances and do not provide a formal approach.

Directions. Important directions include supporting dominance based on (1) organizational context, as in the legal principle of Lex Superior, which says that the decisions of a higher court take precedence over those of a lower court, and (2) temporal recency, as in the legal principle of Lex Posterior, which says that more recent decisions take precedence over earlier ones. Another direction is to provide methods in handling a cycle of dominance relations and in applying priority to a set of dominance relations.

Acknowledgments

We thank the US Department of Defense for support through the Science of Security Lablet grant to NC State University.

References [Alberti et al., 2006] Marco Alberti, Marco Gavanelli, Evelina Lamma, Federico Chesani, Paola Mello, and Paolo Torroni. Compliance veriﬁcation of agent interaction: A logic-based software tool. Applied Artiﬁcial Intelligence, 20(2-4):133 157, February April 2006. [Alechina et al., 2013] Natasha Alechina, Mehdi Dastani,

and Brian Logan. Reasoning about normative update. In Proceedings of the 23rd International Joint Conference on Artiﬁcial Intelligence (IJCAI), pages 20 26, Beijing, August 2013. [Boella and van der Torre, 2008] Guido Boella and Leendert

van der Torre. Institutions with a hierarchy of authorities in distributed dynamic environments. Artiﬁcial Intelligence and Law, 16(1):53 71, March 2008. [Clarke et al., 1986] Edmund M. Clarke, E. Allen Emerson,

and A. Prasad Sistla. Automatic veriﬁcation of ﬁnitestate concurrent systems using temporal logic speciﬁcations. ACM Transactions on Programming Languages and Systems, 8:244 263, April 1986. [Criado et al., 2015] Natalia Criado, Elizabeth Black, and

Michael Luck. A coherence maximisation process for solving normative inconsistencies. Autonomous Agents and Multi-Agent Systems (JAAMAS), June 2015. Online. [Dignum et al., 2005] Frank Dignum, Jan Broersen, Virginia

Dignum, and John-Jules Meyer. Meeting the deadline: Why, when and how. In Michael G. Hinchey, James L. Rash, Walter F. Truszkowski, and Christopher A. Rouff, editors, Formal Approaches to Agent-Based Systems, volume 3228 of Lecture Notes in Computer Science, pages 30 40. Springer, 2005. [Gebser et al., 2014] Martin Gebser, Roland Kaminski, Ben-

jamin Kaufmann, and Torsten Schaub. Clingo = ASP + control: Preliminary report. In Michael Leuschel and Tom Schrijvers, editors, Technical Communications of the Thirtieth International Conference on Logic Programming (ICLP), volume 1433, 2014. [Gelfond, 2008] Michael Gelfond. Answer sets. In Frank

van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, pages 285 316. Elsevier, 2008. [Ghanavati et al., 2014] Sepideh Ghanavati, Llio Humphreys, Guido Boella, Luigi Di Caro, Livio Robaldo, and Leendert van der Torre. Compliance with multiple regulations. In Proceedings of the 33rd International Conference on Conceptual Modeling (ER), volume 8824 of Lecture Notes in Computer Science, pages 415 422. Springer, October 2014. [Governatori et al., 2007] Guido Governatori, Joris Hulstijn,

R egis Riveret, and Antonino Rotolo. Characterising deadlines in temporal modal defeasible logic. In AI 2007:

Advances in Artiﬁcial Intelligence, number 4830 in Lecture Notes in Computer Science, pages 486 496. Springer, 2007. [Ingolfo et al., 2014] Silvia Ingolfo, Ivan Jureta, Alberto

Siena, Anna Perini, and Angelo Susi. N omos 3: Legal compliance of roles and requirements. In Eric Yu, Gillian Dobbie, Matthias Jarke, and Sandeep Purao, editors, Conceptual Modeling, volume 8824 of Lecture Notes in Computer Science, pages 275 288. Springer, 2014. [Knobbout and Dastani, 2012] Max Knobbout and Mehdi

Dastani. Reasoning under compliance assumptions in normative multiagent systems. In Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems, AAMAS, pages 331 340, Valencia, 2012. [Marinovic et al., 2014] Srdjan Marinovic, Naranker Dulay,

and Morris Sloman. Rumpole: An introspective breakglass access control language. ACM Transactions on Information and System Security (TISSEC), 17(1):2:1 2:31, August 2014. [Oren et al., 2008] Nir Oren, Michael Luck, Simon Miles,

and Timothy J Norman. An argumentation inspired heuristic for resolving normative conﬂict. In Proceedings of the 5th Workshop on Coordination, Organizations, Institutions, and Norms in Agent Systems (COIN), pages 41 56, Toronto, 2008. [Prakken and Sergot, 1996] Henry Prakken and Marek Ser-

got. Contrary-to-duty obligations. Studia Logica, 57(1):91 115, 1996. [Singh, 2013] Munindar P. Singh. Norms as a basis for gov-

erning sociotechnical systems. ACM Transactions on Intelligent Systems and Technology (TIST), 5(1):21:1 21:23, December 2013. [Vasconcelos et al., 2009] Wamberto W. Vasconcelos, Mar-

tin J. Kollingbaum, and Timothy J. Norman. Normative conﬂict resolution in multi-agent systems. Autonomous Agents and Multi-Agent Systems, 19(2):124 152, October 2009. [Yolum and Singh, 2004] Pınar Yolum and Munindar P.

Singh. Reasoning about commitments in the event calculus: An approach for specifying and executing protocols. Annals of Mathematics and Artiﬁcial Intelligence, 42(1):227 253, September 2004.