Coco: Runtime Reasoning about Conflicting Commitments

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 specific commitment instances when applied to specific parties in specific situations. In some situations, commitment instances demand conflicting conditions or assignments of resources. We characterize the means for resolving such conflicts 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 conflict 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 conflicts 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] define a CTL variant and present a formalism of deadlines to determine norm compliance based on whether agents bring about specified 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 conflicts between norms as a design problem with a view to specifying schemata (in our terminology) that avoid potential conflicts. In contrast, Coco aims to resolve conflicts as they arise between instances. This has the benefit of only having to deal with conflicts 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 identification 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 conflict. They build conflict graphs with norms and conflicts as nodes and edges. Oren et al. use agent preferences to prune norms in conflict 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 that resolves conflicts among instances of norms by optimization using agent objectives and preferences. The optimization function, built into the conflict-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 conflict 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 specific 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↪ dbtI↪ crdI↪ ti) to mean a commitment instance in which s is the commitment schema that the instance instantiates, dbtI and crdI are the specific debtor and creditor (i.e., the principals who fill 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, gCom, committing guardians to take care of their charges, as open (implicitly universally quantified) FOL formulas. We use capitalized words to represent variables, and lowercase for constants. Statements 2 and 3 mean that if G fills the guardian role for charge C at T, then G is the debtor of the gCom 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 wCom defined 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 wCom instance. The antecedent of wCom 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(gCom)
• 2 guardianR(C↪G↪T) ! dbt(gCom↪G↪T)
• 4 [sick(C↪T) ^ crd(gCom↪C↪T)] ! ant(gCom↪T)
• 3 guardianR(C↪G↪T) ! crd(gCom↪C↪T)
• 5 [bring(G↪C↪ Ped↪T) ^ pedR(C↪ Ped↪T) ^dbt (gCom↪ G↪ T ) ^ crd (gCom↪ C ↪ T )]
• 6 dDuration(gCom↪ 3)
• ! con(gCom↪ T )

Listing 1: Definition of the gCom schema

• 1 schema(wCom)
• 2 employer(Ee↪ Er↪T) ! dbt(wCom↪ Ee↪T)
• 4 [dbt(gCom↪ Ee↪T) ^ crd(wCom↪ Er↪T) ^workhour (Ee ↪ Er ↪ T )] ! ant (wCom↪ T )
• 3 guardianR(C↪G↪T) ! crd(wCom↪ Er↪T)
• 5 [dbt(wCom↪ Ee↪T) ^ crd(wCom↪ Er↪T)
• 6 dDuration(wCom↪ 0)

^atWork (Ee ↪ Er ↪ T )] ! con(wCom↪ T )

Listing 2: Definition of the wCom schema

We treat compliance and conflict with respect to instances. Thus, if Alice falls sick at time instant T , an instance of gCom is instantiated and becomes detached at T. If Bob takes Alice to her pediatrician within three hours, then the instance is satisfied. Otherwise, the instance is violated.

3 Formal Language andModel

Coco's formal language is the function-free first-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 finite interval, and durations; (2) predicates naming roles of organizations, such as guardianR, 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(gCom↪ bob↪ alice↪ 10), which we abbreviate to gComInst in the following, names an instance of gCom with debtor bob and creditor alice detached at time 10. Similarly, the term instance(wCom↪ bob↪ steve↪ 11), abbreviated henceforth as wComInst , names an instance of wCom.

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 gComInst in Listing 3.

1 [sInst(gComInst)^isInstOf (gComInst↪ gCom)] ! crdI (gComInst ↪ alice) 2 [sInst(gComInst)^isInstOf (gComInst↪ gCom)] ! dbtI (gComInst ↪ bob) 3 dDurationI (gComInst↪ 3)

The antecedent and consequent of an instance, omitted in the listing, are formed by substituting the names of specific 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 sInst specify the corresponding types; isInstOf identifies the schema of an instance; and antI and conI state that instance antecedents and consequents hold at specific times.

The satisfaction of an instance is formalized as becomesSat(Si↪ T), which means that T is the first time at which the consequent of Si holds, provided this happens before the deadline; satisfied is true of the instance from that time on. The violation of an instance is realized in a similar way. Specifically, the statement becomesViolated(Si↪ T) holds at T when Si is detached, but not dominated, and its consequent does not hold within the deadline. The definitions for becomesSat and becomesViolated are provided in Listing 4. The predicate conINotHold(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 ) ^ conI (Si↪T) ^ di↵erence(T↪T 0 ↪ 1)] ! becomesSat (Si ↪ T ) 2 [becomesDetached(Si↪T1 ) ^ dDurationI (Si↪T2 ) ^addition(T1 ↪ T2 ↪ T ) ^ conINotHold (Si ↪ T1 ↪ T ) ^≻dominated (Si ↪ T )] ! becomesViolated (Si ↪ T )

We define a set of instances as conflicting 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 specific scenarios. Section 5 formalizes knowledge showing how gComInst and wComInst conflict in our example. Listing 5 defines conflicting(Si1↪ Si2↪ T) symmetrically as holding at time T in case Si1 and Si2 are detached but their consequents cannot both hold at T .

Listing 5: The conflicting relation

In Example 1, Bob is required to be at his workplace during work hours and at Carol's office with Alice when Alice is sick. If Alice gets sick during Bob's work hours, both gComInst and wComInst detach and require Bob to be in two places at the same time. The consequent conditions conflict even when Alice is not sick, but only matter for detached instances; only then may such conflicts cause a commitment violation.

We resolve such conflicts 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 irreflexive. A partial order is appropriate because changing commitments and unforeseen conflicts may make a total ordering infeasible; a partial order can suffice to resolve conflicts 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 conflicting instance in the same set.

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

1 [isInstOf (Si1 ↪ gCom) ^ isInstOf (Si2 ↪ wCom) ^detached (Si1 ↪ T ) ^ detached (Si2 ↪ T ) ^sameDbtI (Si1 ↪ Si2 ) ^ sameCrdI (Si1 ↪ Si2 )] ! dominates (Si1 ↪ Si2 ↪ T )

Listing 7 defines dominated(Si1↪ T) to hold at T in case a detached instance Si1 is in conflict with another detached, nondominated instance Si2 that dominates it at T.

1 [dominates(Si2 ↪ Si1 ↪T) ^ conflicting(Si1 ↪ Si2 ↪T) ^≻dominated (Si2 ↪ T ) ^ detached (Si1 ↪ T ) ^detached (Si2 ↪ T )] ! dominated (Si1 ↪ T )

4 Decision Procedures, Theoretical Results

Given a Coco snapshot of the current enactment, specifically 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.

Definition 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 conflict; and
• (b) It is not possible to infer fromS the fact that nii conflicts 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 satisfies 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 conflict 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 fromS the fact that nii conflicts 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 conflict 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 modelsMandM0 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 gCom dominates wCom 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 definitions.

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 definition of D, for each element nii of D one cannot infer from S that nii is in conflict with another detached instance that dominates it. Further, D includes all the instances in S that satisfy the condition (a) in Definition 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 definitions 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 defined above. By definition 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 conflict 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 definition of associated set forM0 , 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 finding 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 systemM with initial state s, a finite 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 workflow and formalize conflict 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 gComInst. Then at time 11, the middle node (labeled 11) indicates detachment of wComInst. Node 11b says wComInst becomes satisfied if Bob is at work at 11. Similarly, 11a says gComInst becomes satisfied if Bob brings Alice to her pediatrician at time 11. A conflict occurs at time 11 because Bob cannot be at two places at once, assuming Carol's office is at hospitalLoc, Bob's work is at companyLoc, and the two are distinct. Finally, node 13 indicates that with the conflict detection and dominance relation, gComInst would not become violated even if Bob did not bring about the consequent.

In summary, Coco finds that gComInst dominates wComInst at time 11; gComInst is satisfied 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 finds that gComInst is violated at time 13 and wComInst is satisfied at 11. The nondominated instances remain violated if their consequents do not hold within the deadline, whereas a dominated instance may be satisfied.

Listing 8 formalizes the conflict 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 wComInst's consequent cannot be true at T when gComInst's consequent holds at T . Lines 5-7 handle the converse. Thus, gComInst and wComInst instances conflict and the latter is dominated.

1 [atLocation(P↪ L1 ↪T) ^ (L1 6= L2 )] ! ≻atLocation(P ↪ L2 ↪ T ) 2 [isInstOf (Si↪ gCom) ^ conI (Si↪T) ^ dbtI (Si↪G)] ! atLocation(G↪ hospitalLoc↪ T ) 3 [employerR(Ee↪ Er↪T) ^≻atLocation(Ee ↪ companyLoc↪ T )] ! ≻atWork (Ee ↪ Er ↪ T ) 4 [isInstOf (Si↪ wCom) ^ dbtI (Si↪ Ee) ^ crdI (Si↪ Er) ^≻atWork (Ee ↪ Er ↪ T )] ! ≻conI (Si ↪ T ) 5 [isInstOf (Si↪ wCom) ^ conI (Si↪T) ^ dbtI (Si↪ Ee) ^crdI (Si ↪ Er )] ! atLocation(Ee ↪ company ↪ T ) 6 [guardianR(C↪G↪T) ^ pedR(C↪ Ped↪T) ^≻atLocation(G↪ hospitalLoc↪ T )] ! ≻bring (G↪ C ↪ Ped ↪ T ) 7 [isInstOf (Si↪ gCom) ^ dbtI (Si↪G) ^ crdI (Si↪C) ^pedR(C ↪ Ped ↪ T ) ^ ≻bring (G↪ C ↪ Ped ↪ T )] ! ≻conI (Si ↪ T )

5.2 Additional Dominance Relations

Dominance relations can be specified incrementally to cover conflicts 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 modified 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 gCom, namely instance(gCom, amy, alice, 10), abbreviated gComInst2. We want gComInst2 to dominate gComInst because Amy is currently available but Bob is not. We formalize this availability-dependent dominance relation in Listing 9. Specifically, a detached instance Si1 of gCom dominates another detached instance Si2 of gCom 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 [isInstOf (Si1 ↪ gCom) ^ isInstOf (Si2 ↪ gCom) ^detached (Si1 ↪ T ) ^ detached (Si2 ↪ T ) ^sameCrdI (Si1 ↪ Si2 ) ^ dbtI (Si1 ↪ G1 ) ^dbtI (Si2 ↪ G2 ) ^ (G1 6= G2) ^available(G1 ↪ T ) ^ ≻available(G2 ↪ T )] ! dominates (Si1 ↪ Si2 ↪ T )

In Example 2, gComInst2 is nondominated. However, gComInst2 dominates and conflicts with gComInst, so gComInst is dominated. As before, gComInst dominates wComInst, so by transitivity, gComInst2 dominates wComInst. Although gComInst still conflicts with wComInst, wComInst is nondominated because gComInst is dominated and because it does not conflict with gComInst2.

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 [isInstOf (Si1 ↪ gCom) ^ isInstOf (Si2 ↪ gCom) ^detached (Si1 ↪ T ) ^ detached (Si2 ↪ T ) ^sameCrdI (Si1 ↪ Si2 ) ^ crdI (Si1 ↪ C ) ^dbtI (Si1 ↪ G1 )^dbtI (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 )

6 Discussion

Coco provides a flexible formalization of instances, including reasoning about conflicts 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 conflicts 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 justification 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 defining 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.