PL is a low-complexity fragment of OWL2, expressly designed to automatically check the compliance of privacy policies with respect to the consent of data subjects and the regulations on personal data processing, such as the GDPR. Privacy policies, consent and regulations can all be expressed uniformly with PL classes, and compliance checking is reduced to subsumption checking. The latter is tractable and highly scalable to meet the performance requirements of some applications. Several use cases need negation in the queries; however, subsumption checking becomes coNP-hard, even if negation is restricted to atomic concepts. In this paper we show that an alternative encoding based on histories of positive and negative policies (where negation is applied to compound concepts) can be processed in polynomial time by a correct and complete algorithm.
PL is a recently introduced fragment of SROIQ (D) that is being successfully used to encode privacy policies, the consent of data subjects, and objective parts of the GDPR [4, 5]. It is also being used to encode licenses formulated with a pro le of ODRL1 and with JSON; well-de ned translations from these formats to PL provide the formal semantics of licenses. The main goal of PL is enabling automated compliance checks for data economies. Many companies are interested in such tools, that help in preventing sanctions and reputation loss.
PL supports simple ontologies that de ne privacy-related and licensingrelated vocabularies.2 Policies, consent, regulations, and licenses are encoded as classes; compliance checking is reduced to subsumption checking over such classes.
PL balances expressiveness with usability and scalability. In some use cases, it should be possible to execute a few thousands compliance checks per second; ? This work is funded by the European Union with grant n. 883464. Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 1 https://w3c.github.io/market-data-odrl-pro le/md-odrl-pro le.html 2 Currently, the reference vocabularies for privacy are those de ned by the DPVCG group of the W3C, see https://www.w3.org/community/dpvcg/. experiments show that a specialized engine implemented in Java can check the compliance of typical privacy policies with respect to the available consent in about 400-500 -seconds [5]. Concerning usability, SPECIAL's use case partners have successfully veri ed that their employees can write correct privacy policies.
The use cases of the H2020 project SPECIAL3 { that developed the rst version of PL { and its ongoing follow-up TRAPEZE4 call for extensions of PL. Here we focus on negation, that is also needed in the licensing domain. Negation has three main applications in these contexts: { expressing exceptions to a general policy/license; the resulting policies are more compact and readable; { supporting the right of the data subjects to withdraw or restrict their consent to data processing; { supporting dynamic consent [8].
In dynamic consent, users are asked for consent immediately before data are collected. Users may reply within a speci ed timeout, after which consent is implicitly assumed. Users may deny consent either within the timeout or later, by revising such implicit consent statements. In all cases, it is useful to formalize statements such as \location can be tracked in Naples, but not in Via Roma".
This paper investigates how to introduce SROIQ's complement operator `:' in PL without a ecting its tractability and scalability. The main contributions are the following: 1. we prove that the simplest way of introducing negation in PL makes reasoning coNP-hard; 2. then we introduce a notion of history that addresses the above use-case requirements and can be processed in polynomial time.
The paper is organized as follows: In the next section, we recall the basic de nitions and properties of PL, illustrate it with some examples, and list related complexity results. Section 3 proves that PL with atomic negation in the queries is intractable. Section 4 introduces histories and proves that compliance checking based on histories is tractable. Section 5 reports our conclusions. 2
We assume the reader to be familiar with the syntax and the model-theoretic semantics of description logics, and refer to [3] for all de nitions. As usual, if I is an interpretation, then we denote its domain and its interpretation function with I and I , respectively.
The axioms supported by PL knowledge bases are those illustrated in Table 1. PL queries are inclusions C v D where C and D are full PL concepts, that is, unions of the form:
C1 t : : : t Cn 3 https://specialprivacy.ercim.eu/ 4 https://trapeze-project.eu/
A v B disj(A; B)
I j= AI i :
BI
AI \ BI = ; range(R; A) (x; y) 2 RI ! y 2 AI func(R)
(x; y) 2 RI ^ (x; z) 2 RI ! y = z where each Ci is a simple PL concept. Such concepts are de ned by the following grammar:
C ::= A j 9R:C j 9F:[l; u] j C u C where A is a concept name, R is a role name, F is an integer-valued concrete feature (i.e. a data property, in OWL2 terminology), and l; u are integers. The meaning of 9F:[l; u] is: (9F:[l; u])I = d 2
I j 9i 2 Z:(d; i) 2 F I ^ l i u (recall that for all integer-valued concrete features F and all interpretations I, F I I Z). 2.1
A company { call it BeFit { sells a wearable tness appliance and wants to:
(i) process biometric data (stored in the EU) for sending health-related advice
to its customers, and (ii) share the customer's location data with their friends.
Location data are kept for a minimum of one year but no longer than 5; biometric
data are kept for an unspeci ed amount of time. In order to carry out these
two data processing activities legally, BeFit needs consent from its European
customers. Formally, the encoding of BeFit's privacy policy P in PL looks as
follows:
(9has purpose:FitnessRecommendation u 9has data:BiometricData u
9has processing:Analytics u 9has recipient:BeFit u
9has storage:9has location:EU)
t
(9has purpose:SocialNetworking u 9has data:LocationData u
9has processing:Transfer u 9has recipient:DataSubjFriends u
9has storage:9has duration:[y1; y5]) :
Note that P is the union of two sub-concepts that formalize operations (i) and
(ii). Here y1 and y5 stand for the integer representation of one year and ve
years, respectively.
(
A consent policy C, that speci es the class of operations that a data subject
permits, is encoded in a similar fashion. Then, P complies with C i K j= P v C,
where K is the knowledge base that de nes the terms used in the policies. For
example, the consent policy of a user that opts out (ii), and opts in (i) only for
anonimized data, can be encoded as follows:
(9has purpose:FitnessRecommendation u 9has data:BiometricData u
9has processing:Analytics u 9has recipient:BeFit u
9has storage:9has location:EU) :
Clearly, BeFit's privacy policy P complies with this consent policy. As a second
example, suppose that the data subject allows analytics on anonimized biometric
data. This policy can be formalized as follows:
(
The knowledge base K typically contains both domain-speci c axioms and domain-independent axioms, that represent general properties of the business policies. The latter axioms specify, for instance, that the primary roles has purpose, has data, has processing, and has storage are functional, and range over suitable, pairwise-disjoint concepts: range(has purpose; AnyPurpose) range(has data; AnyData) disj(AnyPurpose; AnyData) : : :
HeartRate v BiometricData ;
ComputeAvg v Analytics : Domain-speci c axioms can be used to instantiate the compliance framework in a particular application domain. For example, in our scenario, domain-speci c data categories and processing can be introduced with inclusions like: These two axioms, together with the above consent, allow BeFit to compute the average heart rate of the data subject in order to send her tness recommendations. Other typical axioms specify which classes are mutually disjoint, as in:
disj(BiometricData; LocationData) :
Note that negation is not supported in this language, so there is no explicit way of denying consent, nor is it possible to introduce exceptions to a general consent. Two alternative ways of introducing negation in PL's representation of policies will be discussed in sections 3 and 4. 5 We are assuming that K does not entail BiometricData v Anonymized.
In this section we report some de nitions and results from [4] that will be useful in Section 4.
De nition 1. A PL query C v D is interval safe if, for all constraints 9f:[l; u] occurring in C and all 9f:[l0; u0] occurring in D, either [l; u] [l0; u0] or [l; u] \ [l0; u0] = ; .
Every PL query C v D is equivalent to an interval safe inclusion C v D, where j= C C [4, Prop. 5]. Informally speaking, when subsumptions are interval safe, then they behave as in a convex logic. Formally, interval safe queries enjoy the following property, that follows from lemmas 1 and 2 of [4], combined with Propositions 1 of the same paper: Lemma 1. Let K be a PL knowledge base and let C be a simple PL concept such that K 6j= C v ?. There exist an interpretation I and an individual d 2 I such that: a) I j= K ; b) d 2 CI ; c) for all interval safe PL queries C v D, d 2 DI i K j= C v D .
We will call such pairs (I; d) canonical models of K and C. The above lemma implies the following convexity property : Proposition 1. for all PL knowledge bases K, and all interval safe PL queries q = (C v D1 t : : : t Dn) where C is simple, K j= q i there exists i such that K j= C v Di (1 i n). 2.3
Deciding whether a full PL concept is inconsistent with respect to a PL knowledge base is in P. Deciding whether a PL query is a logical consequence of a PL knowledge base is in general coNP-complete. It is in P if, for all simple PL concepts Ci occurring on the left-hand side of the subsumption query, the number of concrete features occurring in Ci is bounded by a constant c. In SPECIAL and TRAPEZE's privacy policies, c = 1. With this bound, a sequential Java implementation can reach over 2000 compliance checks per second, thereby addressing the scalability requirements posed by the use case partners of SPECIAL and TRAPEZE [5].
The above complexity results { that have been proved in [4] { have been extended in [5] to knowledge bases K [ O where K is a PL knowledge base and O is a Horn-SRIQ knowledge base, under the following assumptions: 1. O belongs to a tractable fragment of Horn-SRIQ; 2. none of the roles occurring in O occurs in either K or the given PL query.6 6 With suitable syntactic sugar, the roles de ned in O may be used in the queries, provided that the roles de ned in K do not occur within the scope of those de ned in O [5, Remark 5.1].
Note that PL knowledge bases are in OWL2-RL, a Horn fragment of OWL2; they are also in the extensions of E L and DL-litehHorn with functional roles. Answering PL subsumption queries is equivalent to solving query containment problems with respect to PL knowledge bases, where the queries are the translation of full PL concepts into formulae of rst-order logic. Such formulae are instances of the class of queries investigated in [9], called extended faceted queries. More precisely, the queries derived from full PL concepts are unions of conjunctive queries with comparison operators (in our case only ` ', that is needed to express interval membership). In the following sections, such queries will be extended with negation.7 The comparison operator makes the usual reduction of query containment to query answering impossible, so the literature on answering unions of conjunctive faceted queries is not directly applicable to our case. For more details { and further tractability and intractability results concerning faceted queries { see [5, Sec. 5.3].
In the extension of E L with functional roles, subsumption checking is complete for EXPTIME, in general [2]. A tractability result for empty TBoxes is reported in [6, Fig. 4]; however, in the same paper, it is proved that even with acyclic TBoxes, subsumption is coNP-complete. The tractability of an extension of E L with non-convex concrete domains (like intervals) has been proved in [6], under the assumption that the TBox is a set of de nitions of the form A C, where each A is a concept name and appears in the left-hand side of at most one de nition.
If DL-litehHorn is extended with functional roles, then the data complexity of query answering raises at the rst level of the polynomial hierarchy and knowledge base satis ability becomes EXPTIME-complete [1].
Finally, a result relevant to the extension of queries with negation discussed in the following sections. Rosati [7] proved that answering conjunctive queries with safe negation in DL-lite is coNP-hard. The proof makes use of a knowledge base that contains negation and inverse roles. In our setting, queries are intractable even when the knowledge base is empty. 3
Intractability of P L with Atomic Negation
With reference to the example illustrated in Section 2.1, assume that a
BeFit customer wants to restrict her consent, by precluding that locations in her
homeplace (say Rome) are shared with friends. A simple way of introducing this
restriction in (
RomeLocationData v LocationData : 7 We will actually work on the subsumption problems that correspond to containment problems involving unions of conjunctive queries with ` ' and negation. This encoding extends PL queries with atomic negation (that is, negation applied to concept names). Our use cases do not need negation in PL knowledge bases.
Subsumption checking over full PL concepts with atomic negation can be reformulated as query containment over unions of conjunctive queries with safe negation. Containment of conjunctive queries with negation is 2p-complete [10], so the intractability of PL with atomic negation in the queries does not come as a surprise.
Here we show that subsumption checking remains intractable (coNP-hard) even if atomic negation is used as in the above example verbatim, that is, in existential restrictions of the form
9R:(A u :B) i=1 where A; B are concept names. The reduction is from the validity of 3-DNF formulae. Given such a propositional formula = Win=1(Li;1 ^ Li;2 ^ Li;3), its reduction is:
n
9R:A v G 9R:(A u Li;1) u 9R:(A u Li;2) u 9R:(A u Li;3)
where R is any role name and A is a concept name that does not occur in any
Li;j . It is not hard to see that is valid i the above inclusion is valid, and that
the reduction can be computed in polynomial time (actually, logarithmic space),
so the following theorem holds:
Theorem 1. Subsumption checking in PL with atomic negation is coNP-hard
even if the knowledge base is empty and negation is restricted to concepts of the
form (
Our use cases can also be addressed by modeling the sequence of consent and denial statements issued by the data subject (either through the dynamic consent system or through the dashboards for personal data control). In formal terms, each such statement is a simple policy with a sign, that speci es whether the operations described by the policy are permitted or forbidden. In case of con icts, older statements are overridden by more recent statements.
each Ci is a simple PL concept.
C2 : : : Cn where Histories are just a handy way of representing compound concepts with negation, as shown by the following inductive translation tr, where H is a history: history tr(history) +C
C H+C tr(H) t C H
C tr(H) u :C
Hereafter, we will identify each history H with the corresponding concept tr(H).
Example 1. Consider the example in Section 3 and let H be the history +D1 +
D2 D3, where D1 and D2 are the two arguments of the union in (
9has data:(RomeLocationData) : By the distributivity of u on t, H is equivalent to (D1 u :D3) t (D2 u :D3). Note that D1 u :D3 is equivalent to D1, because D1 and D3 are disjoint. This follows from three facts: (i) LocationData and BiometricData are disjoint, (ii) RomeLocationData is a subclass of LocationData, and (iii) has data is functional. Concerning D2 u :D3, by (iii) we have that the concept
9has data:(LocationData) u :9has data:(RomeLocationData)
is equivalent to
9has data:(LocationData u :RomeLocationData) :
(
K j= C v H where K is a PL knowledge base, C is a full PL concept, and H is a history, can be decided in polynomial time. For this purpose, we need a few preliminary de nitions and lemmas. First, we normalize H with the following procedure8: De nition 3 (Normalization norm(H)). Let H = +C1 C2 : : : Cn be a history, K be a knowledge base, and C be a concept. The normalization of H w.r.t. K and C, denoted by normK;C (H), is obtained with the following three steps: a) replace each Ci in H with will be denoted by H # C;
(Ci u C); the result of this transformation b) remove from H # C all elements
D such that K j= D v ? ; c) remove from the resulting history all the elements element D0 such that K j= D v D0 .
D followed by some
The subscripts K and C in normK;C (H) will be omitted when clear from context.
The above normalization preserves the entailments of the form (
K j= C v H i K j= C v norm(H) .
The proof of the above lemma is based on the next lemma: Lemma 3. Let K be a PL knowledge base, let C be a full PL concept, and let H = +C1 : : : Cn be a history. Then the following propositions hold: a) j= H u C
(H # C) u C ; b) if K j= D v ? then K j= H D
H ; c) if H = H1 CiH2 Cn and K j= Ci v Cn, then K j= H H1H2 Cn.
Proof. (Sketch) We prove Lemma 3.a) by induction on the length of H. In the base case, H = +D, so H u C and (H # C) u C are syntactically the same.
Let H = H0 D. If D occurs positively, we have by distributivity that H uC is equivalent to (H0uC)+(DuC). Moreover, by construction H # C = (H0 # C)+D and hence (H # C) u C is equivalent to ((H0 # C) u C) + (D u C). Then, the assertion follows from the fact that, by (IH), H0 u C and (H0 # C) u C are equivalent. An analogous proof for the negative case is left to reader.
Lemma 3.b) is trivial, so we focus on point c). If Ci and Cn occur
positively in Lemma 3.c) then H1H2+Cn is always subsumed by H1+CiH2+Cn.
The other way round directly follows from the fact that H1+CiH2 is subsumed
by H1H2+Ci and K j= Ci v Cn. Analogously, we can prove the negative case
by inverting the directions of subsumptions. Next, assume that Ci is negative
and Cn positive. Since K j= Ci v Cn, the di erence between the extensions
of H1 CiH2 and H1H2 is always contained in the extension of Cn. It follows
that H1 CiH2 + Cn H1H2 + Cn , so point c) holds. The case in which Ci is
positive and Cn negative is similar. There are no further cases, so the proof is
complete.
tu
Proof of Lemma 2. (Sketch) It su ces to show that each of the three
normalization steps preserves (
K j= C v H i K j= C v H u C
i K j= C v (H # C) u C (by Lemma 3.a)
i K j= C v H # C ,
therefore step a) of De nition 3 preserves (
K j= C v H i K j= C v H0 :
Similarly, it can be proved that the last step preserves (
We are nally ready for the main result: Theorem 2. Let K be a PL knowledge base, C be a simple PL concept, and H be a history such that C v H is interval safe. Then K j= C v norm(H) i the following two conditions hold: a) neg(norm(H)) = ;, and b) there exists D 2 pos(H) = pos(norm(H)) such that K j= C v D. Proof. (() Suppose that a) and b) hold. By b), K j= C v D, and clearly j= D v F pos(H), because D is one of the arguments of the union. Moreover, by a), we have that H = F pos(H). It follows immediately that K j= C v H.
()) We prove the contrapositive. Accordingly, suppose that either a) or b) is false. In the former case, by Lemma 4, K 6j= C v norm(H) and the theorem holds. If b) is false, then by convexity K 6j= C v F pos(H), and by the contrapositive of Proposition 2, K 6j= C v norm(H). tu As a corollary of the above theorem, we obtain the desired tractability result. Corollary 1. Let c be an arbitrary but xed non-negative integer. For all PL knowledge bases K and all subsumption queries q = (C1 t : : : t Cn v H) such that 1. H is a history , 2. each Ci is a simple PL concept (i.e. their union is a full PL concept) , 3. for all i = 1; : : : ; n, the number of subconcepts of the form 9f:[l; u] occurring in Ci is bounded by c , the entailment K j= q can be decided in polynomial time.
Proof. Clearly, K j= q holds i for all i = 1; : : : ; n, K j= Ci v H holds. Thus, it su ces to prove that each of these n entailments can be decided in polynomial time. Due to the bound c on the number of intervals, each of these subsumption can be transformed in polynomial time into an equivalent, interval safe inclusion Ci v H, as shown in [4, Proposition 5]. By Lemma 2, the resulting subsumption tests can equivalently be replaced by
K j= Ci v norm(H) : Now Theorem 2 can be applied to verify the above subsumptions.
The test a) in Theorem 2 takes time O(jnorm(H)j) = O(jHj). Test b) requires answering at most jHj PL queries, each of which takes polynomial time [4, Proposition 6]. So the overall cost of testing the conditions of Theorem 2 is polynomial. We are only left to show that computing norm(H) takes polynomial time. Phase a) takes time jCj jHj. Phase b) requires at most jH # Cj concept consistency tests, each of which takes polynomial time [4, Proposition 8]. Finally, phase c) requires answering at most jH # Cj PL subsumption queries, each of which takes polynomial time. Thus, the overall computation of norm(H) takes polynomial time. tu Remark 1. Note that the proof of tractability relies only on the following properties of PL: 1. the convexity of interval safe PL (Lemma 1 and Proposition 1), that is needed in Theorem 2; 2. the tractability of subsumption query answering in PL with bounded occurrences of intervals.
Therefore, our results apply to all tasks of the form (
In practice, it is not necessary to compute norm(H) explicitly. Consider Algorithm 1, for example. Lines 2{4 check condition b) of Theorem 2. In particular, if the computation reaches line 5, then Ck is the rightmost concept D in H satisfying condition b). The \for" loop at line 5 looks for the elements (Cj u C) of H # C that survive phase b) of the normalization. The loop in lines 7{9 checks whether (Cj u C) survives phase c), too. Note that (Cj u C) is looked for after +Ck, because all the negative elements of H # C on the left of +Ck are eliminated during normalization phase c), due to +Ck itself. Thus, Algorithm 1 returns true i conditions a) and b) of Theorem 2 hold.
Input: K, C, H
where C is a simplePL concept, H = C1 : : : Cn, and C v H is interval safe Output: true if K j= C v H, false otherwise 1 if K j= C v ? then return true
// Condition b) 2 k := n 3 while k > 0 and (sign( Ck) 6= `+0 or K 6j= C v Ck) do k := k 1 4 if k = 0 then return false // else Ck 2 pos(H) and K j= C v Ck // Condition a) 5 for i := k + 1 to n do 6 if sign( Ci) = ` 0 and K 6j= Ci u C v ? then 7 j := i + 1 8 while j n and (sign( Cj ) 6= `+0 or K 6j= Ci u C v Cj ) do 9 j := j + 1 10
if j > n then return false 11 return true 5
Summarizing, PL queries need to be extended with negation, in order to address the use cases related to automated compliance with the GDPR. Atomic negation raises the complexity of subsumption checking (on which compliance checking is based) at least to the rst level of the polynomial hierarchy. This holds even if negation is further restricted to the speci c concept expressions that arise in our reference examples. We have tackled this issue by introducing histories of positive and negated PL concepts. Histories represent in a natural way the consent of data subjects and can be processed in polynomial time with Algorithm 1.
The running time of this algorithm grows quadratically with the length of the history, which is likely to be incompatible with the scalability requirements for PL. Thus, in a forthcoming work, we are going to introduce suitable optimizations. Points b) and c) of Lemma 3 already show how to eliminate redundant elements from a history. Further optimizations may partition histories into a set of disjoint, shorter histories. We are also going to explore compact policy representations, where the common parts of history elements are factorized.