We illustrate an OWL2 fragment properly tailored for the specification of both companies' data protection policies and data subjects' consent to data processing. Assessing a company's policy for compliance with data subjects' consent is then reduced to a subsumption checking. We provide a complete subsumption algorithm which combines tableaux-based and structural-subsumption techniques and show that, under some conditions, it performs in polynomial time.
3 http://data.consilium.europa.eu/doc/document/
ST-5419-2016-INIT/en/pdf
4 https://www.specialprivacy.eu/
5 Such legal bases include public interest, the vital interests of the data subject, signed contracts,
and the legitimate interests of the data controller, just to name a few (cf. GDPR Art. 6).
However, the regulation constrains the applicability of these legal bases with a number of provisos
and caveats as the data minimization principle introduced in Art. 5, and the limitations to the
legitimate interests of the controller rooted in Art. 6.1(f).
fragment specifically designed to balance expressiveness requirements to encode data
usage policies and scalability of reasoning. A first formalization has been presented in
[
More precisely, PL+ enhances PL in the following aspects:
– it extends PL by including role domains in the ontology language and role chain
agreements (R1 Rn = S1 Sm) in the query language;
– it relies on a new subsumption checking algorithm that combines tableaux-based
and structural subsumption reasoning techniques. This algorithm is notably simpler
than the one presented in [
PL+ is tailored to formalize policies regulating the usage of personal data. It can express (i) the policies of data controllers (i.e. the organizations that collect and process personal data), (ii) the selective consent to data usage issued by data subjects, and (iii) parts of the GDPR related to consent management, user rights, and data transfer.
The aspects of data usage that have legal relevance are clearly indicated in several articles of the GDPR. In particular, the main properties of a usage policy that need to be encoded and archived include: – reasons for data processing (purpose); – which data categories are involved; – what kind of processing is applied to the data; – which third parties data are distributed to (recipients); – countries in which the data will be stored (location); – time limits for data erasure (duration).
Here we focus only on the technical aspects needed in this work and refer the reader to
[
A PL+ knowledge base KB is a finite set of axioms of the form func(f ), func(R), dom(R; A), ran(R; A), disj(A; B), and A v B, where A and B are concept names, R is a role name, and f denotes a concrete feature. An interpretation I satisfies an axiom if I satisfies the corresponding semantic condition in Figure 1.
Figure 2 shows the syntax and semantics of PL+ operators which allow to define query concepts. We say that a concept is simple if no disjunction occurs in it. By applying the logical equivalences C1 u (C2 t C3) (C1 u C2) t (C1 u C3) and Name
Syntax 9R:(C1 t C2) 9R:C1 t 9R:C2 any concept C can be reduced in a normal form C1 t t Cn where each Ci is simple (clearly, the normal form can be exponentially longer than C). A pointed interpretation satisfies a concept C, formally I; d j= C, iff d 2 CI . Then, I satisfies C in case I; d j= C for some d 2 I . As usual, KB j= C v D means that CI DI , for all models I of KB .
Example 1. A company – call it BeFit – sells a wearable fitness appliance and wants to process biometric data (stored in the EU) for sending health-related advice to a customer. Furthermore, BeFit wants to share the customer’s location data with a group of enterprises (located in the USA) engaged in a joint economic activity. According to Art. 47 of the GDPR, the transfer of personal data outside of EU is allowed towards recipients that enforce, so-called, binding corporate rules. Location data are kept for a minimum of one year but no longer than 5; biometric data are kept for an unspecified amount of time. In order to do all this legally, BeFit needs consent from its customers. The consent BeFit acquires from a customer may look as follows: (9purpose:F itnessRecommendation u 9data:BiometricData u 9processing:Analytics u 9recipient:BeF it u 9store:9location:EU ) t (9purpose:M onetize u 9data:LocationData u 9processing:T ransf er u
(controller
applyBindingCorporateRulesT o = recipient) u
where integers represent years. Moreover, KB can include the following axioms:
f unc(recipient)
Given the knowledge base, the first disjunct of the above consent allows BeFit to compute the average heart rate of the data subject in order to send her fitness recommendations. The purpose could be further detailed by saying how the data subject is contacted, e.g. “recommendation via SMS”. Then, in the customer’s consent Name bottom conjunction disjunction existential restriction concrete constraint existential chain (R1 restriction 9purpose:F itnessRecommendation should be replaced with something like 9purpose:(F itnessRecommendation u 9contact:SMS) : Note also that, since recipient is a functional role, the chain agreement in the second disjunct imposes to the recipient the application of the controller’s binding corporate rules. tu
An Abox A is a finite set of assertions of the form C(x) and R(x; y), where R is a role name, C is a simple query concept, and x and y belong to a countably infinite set of variable names VR. In particular, we assume that VR contains a distinguished variable x0. An assignment : VR ! I interprets all variables in VR as elements of an interpretation I. Let VRA VR be the set of variable names occurring in A, we say that and 0 agree in A if (x) = 0(x), for all x 2 VRA. Then, a pair I; satisfies an Abox A (formally, I; j= A) iff (i) (x) 2 CI , for all C(x) 2 A, and (ii) ( (x); (y)) 2 RI , for all R(x; y) 2 A.
A pointed interpretation I; d satisfies A (formally, I; d j= A) if I; j= A for some assignment with (x0) = d. We write KB ; A j= C(x) meaning that I; j= A implies I; j= C(x), for all models I j= KB and assignments .
Finally, we say that C (resp. A) and D are interval safe iff for all constraints f : [l; u] occurring in C (resp. for all f : [l; u] s.t. f : [l; u](x) 2 A, for some variable x) and f : [l0; u0] occurring in D, either [l; u] [l0; u0], or [l; u] \ [l0; u0] = ;. 3
Checking whether KB j= C v D is performed in three phases. The first phase preprocesses the concept C. First of all, for each f : [l; u] in C, let x1 < x2 < < xr be the integers that occur as interval endpoints in sub-concept f : [l0; u0] of D and belong to [l; u]. Let x0 = ` and xr+1 = u and replace f [l; u] with the equivalent concept r G f : [xi; xi] t f : [xi + 1; xi+1 1] t f : [xr+1; xr+1]: (1) i=0 Doing so, we ensure that C and D are interval safe. Then, C is translated in the corresponding normal form C1 t t Cn. As a consequence, a knowledge base KB entails Rule !u
if 1. C1 u C2(x) 2 A and 2. fC1(x); C2(x)g 6 A, then set A0 A [ fC1(x); C2(x)g if 1. A(x) 2 A and 2. A v B 2 KB , and 3. B(x) 62 A then set A0 A [ fB(x)g if 1. 9R:C(x) 2 A and 2. for no y fR(x; y); C(y)g A then create a new variable ynew and set A0 A [ fR(x; ynew); C(ynew)g if 1. R(x; y) 2 A and 2. dom(R; A) 2 KB , and 3. A(x) 62 A, then set A0 A [ fA(x)g if 1. R(x; y) 2 A and 2. ran(R; A) 2 KB , and 3. A(y) 62 A then set A0 A [ fA(y)g Rule !func(R) if 1. fR(x; y); R(x; z)g then set A0 A[y=z]
Rule !func(f) if 1. ff : [l; u](x); f : [v; w](x)g A and 2. func(f ) 2 KB then set A0 A [ ff : [max(l; v); min(u; w)]g if 1. (R1 Rn = S1 Sm)(x) 2 A, and 2. there does not exist y1; : : : ; yn 1; z1; : : : ; zm 1; y s.t.
fR1(x; y1); S1(x; z1)g A, Ri(yi 1; yi) 2 A, for i = 1; : : : ; n 1, Sj(zj 1; zj) 2 A, for j = 1; : : : ; m 1, fRn(yn 1; y); Sm(zm 1; yg A then create new variables y1new; : : : ; ynnew1; z1new; : : : ; zmnew1; ynew and set A0 A [ fR1(x; y1new); : : : ; Rn(ynnew1; ynew)g
[ fS1(x; z1new); : : : ; Sm(zmnew1; ynew)g Rule !disj
if 1. fA(x); B(x)g A and 2. disj(A; B) 2 KB then set A0 A [ f?(x)g if 1. f : [l; u](x) 2 A and 2. u < l then set A0 A [ f?(x)g C v D iff KB j= Ci v D, for all i = 1; : : : ; n6.
After the preprocessing phase, the subsumption problem is reduced to checking
whether each simple concept Ci is subsumed by D. For a simple concept Ci, during
the second phase, an Abox A0 is first initialised with a Ci(x0) and then expanded by
exhaustively applying the tableaux rules in Figure 3. The subsumption vacuously holds
if the resulting Abox A contains assertions of the form ?(x) for some x. In contrary
case, the third phase checks whether x0 2 hhDiiA, where hhDiiA is the set of variable
names contained in VRA inductively defined as follows:
6 Note that, differently from the subsumption algorithm presented in [
This may significantly impact on performance since the normalization process might exponentially inflate D.
hhAiiA=fx 2 VRA j A(x) 2 Ag hhD1 u D2iiA=fx 2 VRA j x 2 hhD1iiA \ hhD2iiAg hhD1 t D2iiA=fx 2 VRA j x 2 hhD1iiA [ hhD2iiAg hh9R:DiiA=fx 2 VRA j 9y 2 VRA s.t. R(x; y) 2 A and y 2 hhDiiAg and x 2 hhR1 and x 2 hhS1 and S(z; w) 2 Ag
Sm 1; ziiAg hhR; SiiA=f(y; z) 2 VR2A j 9w 2 VRA s.t. R(y; w) 2 A hhR1
SmiiA=fx 2 VRA j 9(y; z) 2 VR2A s.t. (y; z) 2 hhRn; SmiiA hh ; yiiA=fyg R^k; yiiA=fx 2 VRA j 9w 2 VRA s.t. R^1(x; w) 2 A
and w 2 hhR^2 R^k; yiiAg hhf : [a; b]iiA=fx 2 VRA j 9a0; b0 2 N s.t. f : [a0; b0](x) 2 A
and a a0 b0 bg Note that hhR; SiiA, hhR^1 R^k; yiiA, and hh ; yiiA are only used to support the computation of the set hhR1 Rn = S1 SmiiA of variable names in VRA that satisfies a role chain agreement. Intuitively, hhRn; SmiiA computes the set of pairs (y; z) that are connected to a single variable through the role names Rn and Sm. Then, hhR1 Rn 1; yiiA (resp. hhS1 Sm 1; ziiA) recursively computes the set of variables connected to y (resp. to z) through a role chain R1 Rn 1 (resp. S1 Sm 1).
Thereafter, A ! A0 means that A0 results from the application of a rule in Figure 3 to A. As usual ! denotes the reflexive and transitive closure of the ! relation. A is complete (w.r.t. KB ) if no rule is applicable and is clash-free if it does not contain assertions of the form ?(x). Then, let C be a simple concept and KB a PL+ knowledge base, we say that A is the tableaux of C w.r.t. KB if A is complete and fC(x0)g ! A. Lemma 1. Let A and A0 be two Aboxes over VR s.t. A ! A0. For all models I of KB and d 2 I , we have that I; d j= A iff I; d j= A0.
Proof. First, consider A !func(R) A0 and assume that I; d j= A. This means that for some assignment , with (x0) = d, I; j= A. Since the rule !func(R) is applicable to A, it must be the case that I; j= R(x; y1) and I; j= R(x; y2), for some x; y1; y2 2 VRA and a role R s.t. func(R) 2 K. Futhermore, I j= KB by hypothesis, so (y1) = (y2) and hence I; j= A0. Vice versa, assume that I; d j= A0 and let be the corresponding assignment. Since y2 does not occur in A0, is free to map y2 arbitrarily. Then, in order to satisfy A, it is sufficient to assign (y1) to y2. Since in both directions the assignment of x0 has not changed, we have that I; d j= A iff I; d j= A0.
Regarding the other rules, note that A A0 and hence I; d j= A0 implies I; d j= A by monotonicity. For the opposite direction, assume that I; j= A, where (x0) = d.
Case A !u A0. Since !u is applicable to A, (C1 u C2)(x) must occur in A, for some simple concepts C1; C2 and a variable x 2 VRA. I; j= C1(x) and I; j= C2(x) directly follow from the assumption I; j= A. Consequently, I; j= A0.
Case A !v A0. Since !v is applicable to A, for some atomic concepts A; B and a variable x 2 VRA, A(x) 2 A and A v B 2 KB . Then, from I; j= A and I j= KB , it follows that I; j= B(x) and hence I; j= A0.
Case A !9 A0. From the precondition of the rule !9, we have that 9R:C(x) occurs in A. Moreover, from the assumption I; d j= A, it holds dx 2 (9R:C)I , with (x) = dx, which means that there exists an individual d0 s.t. d0 2 CI and (dx; d0) 2 RI . Since ynew does not occur in A, we can assign (ynew) = d0 and obtain I; j= A0.
Case A !dom A0. From the precondition of !dom, R(x; y) 2 A and dom(R; A) 2 KB . So, any I; satisfying A and KB must also satisfy A(x) and hence A0.
Case A !ran A0. Similar to the previous case.
Case A !func(f) A0. From the precondition of the !func(f) rule, we have that I; satisfy f : [l; u](x) and f : [v; w](x) where, according to KB , f is a function from I to N. Then, given dx = (x), both l f I (dx) u and v f I (dx) w hold which clearly means that max(l; v) f I (dx) min(u; w). Consequently, I; j= A0.
Case A != A0. By assumption I; j= A and (R1 Rn = S1 Sm)(x) 2 A. Let dx be the individual associated to the variable x by . There exist two paths dx; d01; : : : ; d0n 1; d and dx; d010; : : : ; d0m0 1; d s.t. (i) (dx; d01) 2 R1I and (dx; d010) 2 S1I ; (ii) (d0i 1; d0i) 2 RiI , with i = 2; : : : ; n 1; (iii) (d0j0 1; d0j0) 2 SjI , with j = 2; : : : ; m 1; (iv) (d0n 1; d) 2 RnI and (d0m0 1; d) 2 SmI. Since the variables y1new; : : : ; ynnew1; z1new; : : : ; zmnew1; ynew are fresh, we can extend by mapping them to d01; : : : ; d0n 1; d010; : : : ; d0m0 1; d, respectively. I; j= A0 follows by construction.
Case A !disj A0. According to the precondition of !disj, fA(x); B(x)g A and disj(A; B) 2 KB . Then, this case is vacuously satisfied since there does not exist a model I of KB and an assignment that satisfy A.
Case A !f? A0.Vacuously satisfied, otherwise we have l f I (d) u and u < l.
Finally, note that in all of the previous cases has been extended by mapping only fresh variables. The assignment of x0 therefore never changes, hence I; d j= A0. tu
Let A be a complete and clash-free Abox, a canonical model of A is an interpretation JA = ( JA ; JA ) satisfying the following conditions: 1. JA = VRA; 2. AJA = fx 2 VRA j A(x) 2 Ag; 3. RJA = f(x; y) 2 VRA VRA j R(x; y) 2 Ag; 4. if f is non-functional (i.e. func(f ) 62 KB ), then (a) f JA f(x; h) 2 VRA N j 9l; u 2 N s.t. f : [l; u](x) 2 A and l h ug; (b) for each f : [l; u](x) 2 A, there exists at least one l h u s.t. (x; h) 2 f JA ; 5. if f is functional, then (x; h) 2 f JA iff (a) h = maxfl j f : [l; u](x) 2 Ag or h = minfu j f : [l; u](x) 2 Ag; (b) for each h0 6= h, (x; h0) 62 f JA .
Note that all canonical models share the same domain as well as the same interpretation of atomic concepts and roles. Concrete features involve multiple canonical models, in particular condition 4 requires a canonical model to satisfy all assertions f : [l; u](x) for a not functional f occurring in A. Condition 5 associates to a variable x the maximum lower (resp. minimum upper) bound of the intervals relative to x and a functional f .
Lemmas 2 and 3 show that a canonical model JA of A satisfies both A and KB . Lemma 2. Let A be a complete and clash-free Abox, JA a canonical model of A and the identity assignment s.t. (x) = x, for all x occurring in A. Then, JA; j= A. Proof. Clearly, JA and satisfy all assertions A(x) and R(x; y) occurring in A by construction. Moreover, given f : [l; u](x) 2 A corresponding to non-functional feature, by construction there exists a value l h u s.t. (x; h) 2 fAJ (see condition 4). As a consequence, also f : [l; u](x) 2 A is satisfied.
Let f be a functional concrete feature and assume by contradiction that JA; 6j= f : [l; u](x), with f : [l; u](x) 2 A. By construction, fAJ associates to x a single value h which is either maxfl j f : [l; u](x) 2 Ag or minfu j f : [l; u](x) 2 Ag. Consider the first case and let f : [^l; u^](x) be an assertion in A s.t. ^l = maxfl j f : [l; u](x) 2 Ag. From JA 6j= f : [l; u](x) and the fact that l ^l it follows that ^l > u. Moreover, since A is complete, by applying !func(f) to f : [l; u](x) and f : [^l; u^](x) we obtain that f : [max(l; ^l); min(u; u^)](x) is also in A. Then, we have that max(l; ^l) = ^l and min(u; u^) u < ^l. Consequently, by application of rule !f? we would have that ?(x) occurs in A against the hypothesis that A is clash-free. Symmetrically, the assumption that fAJ associates to x the minimum upper bound once again results in ?(x) 2 A. tu Lemma 3. Let A be clash-free and complete w.r.t. KB , then a canonical model JA of A is also a model of KB .
Proof. The proof is by reduction ad absurdum. Assume JA does not satisfy A v B 2 KB . Then by construction, for some variable x 2 VRA, A(x) 2 A and B(x) 62 A. However, in this case !v would be applicable to A. Analogously, the assumptions that JA does not satisfy dom(R) v A 2 KB , ran(R) v A 2 KB and func(R) 2 KB all lead to a contradiction of the hypothesis that A is complete. Finally, for each f s.t. func(f ) 2 KB , fAJ is functional by construction. tu
The following lemmas prove that, under the interval safety assumption, the semantic consequences of a knowledge base and a complete Abox can be computed by hh iiA. Lemma 4. Let A be clash-free and complete w.r.t. KB and D a concept s.t. D and A are interval safe. Then, KB ; A j= D(x) iff JA; x j= D, for all canonical models JA. Proof. For the the left-to-right direction, we already know that each canonical model JA satisfies KB and JA; j= A, where is the identity assignment. Then, KB ; A j= D(x) in particular implies JA; j= D(x) and, since (x) = x, we have that JA; x j= D. The right-to-left direction can be proved by induction on the structure of D.
Case D = A. By definition, JA; x j= A iff x 2 AJA iff A(x) 2 A. Moreover, given a model I of KB and an assignment , the facts that I; j= A and A(x) 2 A imply by definition that I; j= A(x). Hence, KB ; A j= A(x).
Case D = f : [l; u], where f is not functional. We show that if JA; x j= f : [l; u], for all canonical models JA, then A contains an assertion f : [l0; u0](x) with l0 l and u0 u. This clearly ensures that KB ; A j= f : [l; u](x). Let f : [l1; u1](x); : : : ; f : [ln; un](x) be the assertions in A relative to f and x, and assume by contradiction that for all i = 1; : : : ; n [li; ui] 6 [l; u]. Since D and A are interval safe, we have that [li; ui] \ [l; u] = ;. Then, by condition 4a, it follows that JA that does not satisfies f : [l; u], a contradiction.
Case D = f : [l; u], where f is functional. By construction, that all canonical models of A satisfy f : [l; u] means that both ^l = maxf:[l;u](x)2A l and u^ = minf:[l;u](x)2A u lie in the interval [l; u]. Then, on the one hand, being A clash-free ensures that ^l u^ and hence [^l; u^] is an interval contained in [l; u]. On the other hand, since A is complete, f : [^l; u^](x) occurs in A and hence KB ; A j= f : [l; u](x).
Cases D = D1 u D2, D = D1 t D2, D = 9R:D0 and D = (R1 Rn = S1 Sm) follow directly from the definitions and the induction hypothesis. tu Lemma 5. Let A be clash-free and complete w.r.t. KB and D a concept s.t. D and A are interval safe. Then, x 2 hhDiiA iff JA; x j= D, for all canonical models JA. Proof. The proof is by induction on the structure of D.
Case D = A. In this case hhDiiA = AJ , for all canonical models JA.
A
Case D = D1 uD2. We have that JA; x j= D1 uD2, for all JA iff JA; x j= D1, for all JA, and JA; x j= D2, for all JA. By induction, this holds iff x 2 hhD1iiA \ hhD2iiA and hence x 2 hhD1 u D2iiA.
Analogously, the cases when D = D1 tD2, D = 9R:D0 and D = (R1 Rn = S1 Sm) follow directly from the definitions applying the induction hypothesis.
Case D = f : [l; u]. For the left-to-right direction, x 2 hhf : [l; u]iiA means that there exists some l0; u0 s.t. l l0 u0 u and f : [l0; u0](x) 2 A. However, this ensures that KB ; A j= f : [l; u](x) and by Lemma 4 it follows that JA; x j= f : [l; u], for all canonical models of A. For the opposite direction, assume that all canonical models satisfy f : [l; u] in x. As we know from Lemma 4, whether f is functional or not, this ensures that there exists an assertion f : [l0; u0](x) in A with [l0; u0] [l; u]. By construction follows that x 2 hhf : [l; u]iiA. tu
The following theorem shows that the combined subsumption checking algorithm is correct and complete.
Theorem 1. Let KB be a PL+ knowledge base, C a simple concept and D a concept s.t. C and D are interval safe. Then, KB j= C v D iff the tableaux A of C contains a clash or x0 2 hhDiiA.
Proof. For the left-to-right direction, assume by contraposition that A is clash-free and x0 62 hhDiiA. By Lemma 5, we have that JA; x0 6j= D. Then, by Lemmas 3 and 1, JA is a model of KB and JA; x0 j= C. It follows that KB 6j= C v D.
For the opposite direction, if A contains a clash, by Lemma 1 no model of KB satisfies C. Hence, KB j= C v D vacuously holds. Finally, assume that A is clashfree and x0 2 hhDiiA. By Lemmas 5 and 3 we have KB ; A j= D. Let I be a model of KB s.t. I; d j= C. Clearly, by assigning x0 to d, I; d j= C(x0) holds and hence I; d j= A (Lemma 1). Then, I is a model of KB and, since I; d j= A, there exists an assignment s.t. I; j= A. Since KB ; A j= D it follows that I; d j= D tu
Finally, we show that tableaux-based expansion in the second phase together with the structural subsumption in the third phase can be performed in polynomial time. Theorem 2. Let KB be a PL+ knowledge base, C a simple concept and D a concept s.t. C and D are interval safe. Subsumption checking KB j= C v D is PTIME. Proof. With respect to the tableaux construction, we show that the resulting Abox A is polynomial in the size of KB and C. First of all, the number of variable names occurring in A depends on the application of !9 and != rules. Since rule !9 generates a single variable name, rule != generates n + m 1 variables at a time and the total number of their applications is bounded by jCj, it follows that VRA is proportional to jCj.
Being VRA / jCj, it is straightforward to see that rule !u can be applied at most jCj times whereas the number of possible applications of rules !v, !dom, !ran, !func(R), and !disj is bounded by jCj jKB j. Finally, the applications of !func(f) and !f? are at most jCj3 jKB j. Then, the size of the resulting tableaux is polynomial in the size of KB and C and hence the second phase of the subsumption algorithm is performed in polynomial time.
Then, checking x0 2 hhDii incrementally updates the extension of the subconcepts of D over A. Consequently, the third phase can be performed in O(jAj jDj). tu
As said above, in case C is not simple, the preprocessing reduces it in a normal
form C1 t t Cn that can be exponentially longer than C. This in particular may
occur if C and D are not interval safe, due to introduction of disjunctions in the interval
normalization (1), thus making the subsumption checking (see also Theorem 7 in [
However, the subsumption algorithm can be optimized in several ways in order to improve performance. A first optimization concerns the interval normalization. Clearly, the number of resulting interval splits depend on the set of distinct end-points occurring in D. We can reduce this set by using the following syntactic replacements in D: f [l1; u1] t f [l2; u2] f [l1; u1] u f [l2; u2] f [minfl1; l2g; maxfu1; u2g] if [l1; u1] [ [l2; u2] is an interval (2) f [l; u] if l u and f is functional : (3) where l = maxfl1; l2g and u = minfu1; u2g.
Standard optimizations can also be used to speed up the tablaux expansion. For instance, rules !9 and !func(R) can be merged as follows: given 9R:C(x), if R is not functional or x has no R-successor, then !9 is applied as usual. Otherwise, C is added to the (single) R-successor of x. The rule !func(f) can as well be optimized. Let f : [l1; u1]; : : : ; f : [ln; un] be the interval constrains occuring in C that are assigned to a variable x, l the maximum lower bound of fl1; : : : ; lng and u the minimum upper bound of fu1; : : : ; ung. It is easy to see that either u < l, that is C is inconsistent w.r.t. KB , or [l; u] is an interval that by construction is contained in all [li; ui]. Therefore, we can replace f : [l1; u1](x); : : : ; f : [ln; un](x) in A with a single assertion f : [l; u](x). 4
We have introduced the description logic PL+ which allows to formalize the data usage policies adopted by controllers as well as the consent to data processing granted by data subjects. Checking whether the controllers’ policies comply with the available consent boils down to subsumption checking between PL+ concepts.
The frequency of compliance checks can be high, so PL+ has been designed to
address scalability requirements by making the language as simple as possible. As a
consequence, the ontology and the query languages are notably different from each other.
In particular, the ontology language largely intersects some fragments of the EL and
DL-lite families of DLs [
We also presented a subsumption algorithm which, in broad terms, reminds the
structural subsumption algorithm for the description logic underlying CLASSIC [
To the best of our knowledge all previous encodings of policies in KR languages
[
As future work, we are planning to implement the presented algorithm and to
assess its scalability experimentally against real data usage policies provided by
SPECIAL’s industrial partners. Moreover, we are planning to study three further extensions
of PL motivated by SPECIAL’s use cases. Two of them are needed by a novel,
dynamic method for collecting consent. This method is based on fine-grained
authorizations, where the data categories involved consist of single data points (e.g. a specific
location). This can be achieved by introducing nominals in PL. Moreover, the data
subject should be able to deny consent for some of such specific authorizations, which
amounts to introducing some form of negation in the policy language. The third
extension is needed to support so-called sticky policies [
This research is funded by the European Unions Horizon 2020 research and innovation programme under grant agreement N. 731601.