In this paper we consider processes that run over data stored in a relational database. Our setting is that of ontology-based data access (OBDA), where the information in the database is conceptually represented as an ontology and is declaratively mapped to it through queries. We are interested in verifying temporal logic formulas on the evolution of the information at the conceptual level, taking into account the knowledge present in the ontology, which allows for deducing information that is only implicitly available. Specifically, we show how, building on first-order rewritability of queries over the system state that is typical of ontology languages for OBDA, we are able to reformulate the temporal properties into temporal properties expressed over the underlying database. This allows us adopt notable decidability results on verification of evolving databases that have been established recently.
Recent work in business processes, services and databases brought the necessity of
considering both data and processes simultaneously while designing the system. This
holistic view of considering data and processes together has given rise to a line of
research under the name of artifact-centric business processes [
Here we introduce Semantically-Governed Data-Aware Processes (SGDAP), in
which we merge these two approaches by enhancing a relational layer constituted by
a DCDS based system, with an ontology, constituting a semantic layer. The ontology
captures the domain in which the SGDAP is executed, and allows for seeing the data
and their manipulation at a conceptual level through an ontology-based data access
(OBDA) system [
The ontology is represented through a Description Logic (DL) TBox [
When an SGDAP evolves, each snapshot of the system is characterized by a database instance at the relational layer, and by a corresponding virtual ABox, which together with the TBox provides a conceptual view of the relational instance at the semantic layer. When the system is progressed by the process component, we assume that at every time the current instance can be arbitrarily queried, and can be updated through action executions, possibly involving external service calls to get new values from the environment. Hence the process component relies on three main notions: actions, which are the atomic progression steps for the data layer; external services, which can be called during the execution of actions; and a process, which is essentially a non-deterministic program that uses actions as atomic instructions. During the execution, the snapshots of the relational layer can be virtually mapped as ABoxes in the semantic layer. This enables to: (i) understand the evolution of the system at the conceptual level, and (ii) govern it at the semantic level, rejecting those actions that, executed at the relational layer, would lead to a new semantic snapshot that is inconsistent with the semantic layer’s TBox.
In this work, we are interested in verifying dynamic properties specified in a variant
of -calculus [
ontology-based data access (OBDA) framework.
representing binary relations between objects, and attributes, representing binary relations between objects and values. The syntax of concept, role and attribute expressions Here, N , P , and U respectively denote a concept name, a role name, and an attribute name, P denotes the inverse of a role, and B and R respectively denote basic concepts and basic roles. The concept 9R, also called unqualified existential restriction, denotes the domain of a role R, i.e., the set of objects that R relates to some object. Similarly, the concept (U ) denotes the domain of an attribute U , i.e., the set of objects that U relates to some value. Note that we consider here a simplified version of DL-LiteA;id where we distinguish between between objects and values, but do not further deal with different datatypes; similarly, we consider only a simplified version of identification assertions.
assertions, and A is an Abox, i.e., a finite set of ABox assertions. DL-LiteA;id TBox assertions have the following form:
B1 v B2
B1 v :B2 (id B Z1; : : : ; Zn)
R1 v R2 R1 v :R2 (funct R)
U1 v U2 U1 v :U2 (funct U ) From left to right, assertions of the first row denote inclusions between basic concepts, basic roles, and attributes; assertions of the second row denote disjointness between basic concepts, basic roles, and attributes; assertions of the last row denote identification (assertions) (IdA), and global functionality on roles and attributes. In the IdA, each Zi denotes either an attribute or a basic role. Intuitively, an IdA of the above form asserts that for any two different instances o, o0 of B, there is at least one Zi such that o and o0 differ in the set of their Zi-fillers, that is the set of objects (if Zi is a role) or values (if Zi is an attribute) that are related to o by Zi. As usual, in DL-LiteA;id TBoxes we impose that roles and attributes occurring in functionality assertions or IdAs cannot be specialized (i.e., they cannot occur in the right-hand side of inclusions).
and t2 denote individual objects and v1 denotes a value.
objects and values over distinct domains, and that for both we adopt the Unique Name
entailment, satisfaction, and model are as usual [
by terms denoting individuals appearing in the ABox. The domain of an ABox A, denoted by ADOM(A), is the (finite) set of terms appearing in A. A union of conjunctive queries (UCQ) q over a TBox T is a FOL formula of the form 9~y1.conj 1(~x; ~y1) _ _
Each conj i(~x; y~i) in q is a conjunction of atoms of the form N (z), P (z; z0), U (z; z0) where N , P and U respectively denote a concept, role and attribute name of T , and z, z0 are constants in a set C or variables in ~x or y~i, for some i 2 f1; : : : ; ng. The (certain) answers to q over an ontology (T ; A) is the set ans (q; T ; A) of substitutions3
ordering of the free variables of q.
of the free variables of q with constants in ADOM(A) such that q evaluates to true
in every model of (T ; A). If q has no free variables, then it is called boolean, and its
certain answers are true or false. Computing ans (q; T ; A) of a UCQ q over a DL-LiteA;id
ontology (T ; A) is in AC0 in the size of A [
queries of the query language EQL-Lite(UCQ) [
Q ! [q] j :Q j Q1 ^ Q2 j 9x.Q j x = y
where q is a UCQ over T and [q] denotes that q is evaluated under the (minimal)
knowledge operator (cf. [
as the certain answers of the embedded UCQs. Hence, also computing ANS(Q; T ; A) of
an ECQ Q over a DL-LiteA;id ontology (T ; A) is in AC0 in the size of A [
connected to an ontology that represents the domain of interest by a mapping, which
relates database values with values and (abstract) objects in the ontology (c.f. [
Formally, an OBDA system is a structure O = hR; T ; Mi, where: (i) R = fR1; : : : ; Rng is a database schema, constituted by a finite set of relation schemas; (ii) T is a DL-LiteA;id TBox; (iii) M is a set of mapping assertions, each of the form: (~x) ; (~y; ~t), where: (a) ~x is a non-empty set of variables, (b) ~y ~x, (c) ~t is a set of object terms of the form f (~z), with f 2 and ~z ~x, (d) (~x) is an arbitrary SQL query over D, with ~x as output variables, and (e) (~y; ~t) is a conjunctive query over T of arity n > 0 without non-distinguished variables, whose atoms are over the variables ~y and the object terms ~t.
stores and manipulates data concerning students and their degree. In particular, we define an OBDA system O = hR; T ; Mi to capture the conceptual schema of such a domain, how data are concretely maintained in a relational database, and how the two information levels are linked through mappings. The conceptual schema is depicted in Figure 1, and formalized as the following DL-LiteA;id TBox T :
Bachelor v Student
Master v Student Graduated v Student (MNum) v Student Student v (MNum) (funct MNum) (id Student MNum)
Bachelor Master
Student mNum: String
Graduated a concrete underlying data source that obeys the database schema R, constituted by the following relation schemas: (i) ENROLLED(id; name; surname; type; endDate) stores information about students that are currently (endDate=NULL) or were enrolled in a bachelor (type="Bachelor") or master (type="Master") course. (ii) GRAD(id; mark; type) stores data of former students who have been graduated. (iii) TRANSF M(name; surname) is a temporary relation used to maintain information about master students that have been recently transferred from another university, and and the conceptual schema T is specified through the following set M of mappings: must still complete the enrollment process. The interconnection between the database schema R m1 : SELECT name; surname; type FROM ENROLLED WHERE type ="Bachelor" ; Bachelor(stu1(name; surname; type)) ; Master(stu1(name; surname; type)) m2 : SELECT name; surname; type FROM ENROLLED WHERE type ="Master" m3 : SELECT name; surname; type; id FROM ENROLLED ; MNum(stu1(name; surname; type); val(id)) m4 : SELECT name; surname FROM TRANSF M ; Master(stu1(name; surname; "Master")) m5 : SELECT e:name; e:surname; e:type FROM ENROLLED e; GRAD g WHERE e:id = g:id ; Graduated(stu1(name; surname; type))
Intuitively, m1 (m2 resp.) maps every id in ENROLLED with type "Bachelor" ("Master") to a bachelor (master) student. Such a student is constructed by “objectifying” the name, surname and course type using variable term stu1=3. In m3, the MNum attribute is instead created using directly the value of id to fill in the target of the attribute. Notice the use of the val function symbol for mapping id to the range of MNum. Mapping m4 leads to create further master students by starting from the temporary TRANSF M table. Since such students are not explicitly associated to course type, but it is intended that they are "Master", objectification is applied to students’ name and surname, adding "Master" as a constant in the variable term. Notice that, according to the TBox T , such students have a matriculation number, but its value is not known (and, in fact, no mapping exists to generate their MNum attribute). Finally, m5 generates graduated students by selecting only those students in the ENROLLED table whose matriculation number is also contained in the GRAD table. tu m = (x) ; (y; t) in
M is m(D) =
S
v2eval( ;D)
Given a database instance D made up of values in V and conforming to schema R and given a mapping M, the virtual ABox generated from D by a mapping assertion [x=v], where eval ( ; D) denotes the evaluation of the SQL query
over D, and where we consider [x=v] to be a set of atoms (as opposed to a conjunction). Then, the ABox generated from D for ABoxes, the active domain ADOM(D) of a database instance D is the set of values by the mapping M is M(D) = S
m2M occurring in D. Notice that ADOM(D) m(D). Notice that ADOM(M(D))
C
. As V
. Given an OBDA system O = hR; T ; Mi (T ; M(D)). We say that O wrt D is satisfiable if it admits a model wrt D. and a database instance D for R
, a model for O wrt D is a model of the ontology
fBachelor(stu1(john; doe; Bachelor)); MNum(stu1(john; doe; Bachelor); val(123))g.
Example 2. Consider a database instance D = fENROLLED(123; john; doe; Bachelor; NULL)g.
The corresponding virtual ABox obtained from the application of the mapping M is M(D) =
tu
compute the certain answers of q over O wrt a database instance D for R
An UCQ q over an OBDA system O = hR; T ; Mi is simply an UCQ over T . To
, we follow a
three-step approach: (i) q is rewritten to compile away T , obtaining qr = REW(q; T );
(ii) the mapping M is used to unfold qr into a query over R, denoted by UNFOLD(qr; M),
which turns out to be an SQL query [
A Semantically-Governed Data-Aware Process (SGDAP) S = hO; P; D0i is formed by an OBDA System O = hR; T ; Mi by a process component P database instance D0 that conforms to the relational schema R in O. Intuitively, the
evolves such data, starting from the initial database D0. progresses the data layer, and may involve external service calls; (iii)
Formally, P = hF ; A; i, where: (i) F is a finite set of functions representing calls to external services, which return values; (ii) A is a finite set of actions, whose execution is a finite set of condition-action rules that form the specification of the overall process, which tells at any moment which actions can be executed.
An action 2
A has the form (p1; : : : ; pn) : (i) (p1; : : : ; pn) is the signature of the action, constituted by a name p1; : : : ; pn of input parameters that need to be substituted with values for the execution effects are assumed to take place simultaneously. Each ei has the form q of the action, and (ii) fe1; : : : ; emg is a set of effect specifications, whose specified Ei, where: (a) qi+ ^Q constants from ADOM(D0). The query qi+ is a UCQ, and the query Q FO formula whose free variables are included in those of qi+. Intuitively, qi+ selects the i is an arbitrary i is a query over R whose terms are variables ~x, action parameters, and i+ ^ Q i tuples to instantiate the effect, and Q
i filters away some of them. (b) Ei is the effect, i.e., a set of facts for R
, which includes as terms: terms in ADOM(D0), input parameters, free variables of qi+, and in addition Skolem terms formed by applying a function f 2 F to one of the previous kinds of terms. Such Skolem terms involving functions represent external service calls and are interpreted so as to return a value chosen by an external fe1; : : : ; emg, where: and a sequence user/environment when executing the action.
The process is a finite set of condition-action rules Q 7! , where is an action and whose other terms can be quantified variables or values in ADOM(D0). in A and Q is a FO query over R whose free variables are exactly the parameters of , Example 3. Consider the OBDA system O defined in Example 1. We now define a process component P = hF ; A; i over the relational schema R of O, so as to obtain a full SGDAP.
– ENROLLED(id; ; ; ; NULL) – TRANSF M(name; surname)
COMPL-ENR(name; surname)
The first rule extracts a matriculation number id of a currently enrolled student (endDate=NULL) from the ENROLLED relation and graduates the student, whereas the second rule selects a pair name surname in TRANSF M and use them to complete the enrollment of that student. In order to be effectively executed, the involved actions rely on the following set F of service calls: (i) today() returns the current date; (ii) getMark(id; type) returns the final mark received by student id; (iii) getID(name; surname; type) returns the matriculation number for the name-surname pair of a student. The two actions GRADUATE and COMPL-ENR are then defined as follows:
COMPL-ENR(n; s) : f GRAD(id; m; t)
GRAD(id; m; t); GRADUATE(id) : f GRAD(id2; m; t)
TRANSF M(n; s) ENROLLED(id; n; s; t; NULL) ENROLLED(id2; n; s; t; d) ^ id2 6= id ENROLLED(id; ; ; t; NULL)
GRAD(id2; m; t); TRANSF M(n; s);
ENROLLED(id2; n; s; t; d); ENROLLED(id; n; s; t; today());
GRAD(id; getMark(id; t); t) g; ENROLLED(id; n2; s2; t; d)
ENROLLED(id; n2; s2; t; d); TRANSF M(n; s) TRANSF M(n2; s2) ^ (n2 6= n _ s2 6= s)
TRANSF M(n2; s2);
ENROLLED(getID(n; s; "Master"); n; s; "Master"; NULL)g
Given a matriculation number id, action GRADUATE inserts a new tuple for id in GRAD, updating at the same time the enrollment’s end date for id in ENROLLED to the current date, while keeping all other entries in TRANSF M; GRAD and ENROLLED. Given a name and surname, action COMPL-ENR has the effect of moving the corresponding tuple in TRANSF M to a new tuple in ENROLLED, for which the matriculation number is obtained by interacting with the getID service call; all other entries TRANSF M; GRAD and ENROLLED are preserved. tu 4
nondeterministically, i.e., two calls of a service with the same arguments may return different results during the same run. This captures both services that model a truly nondeterministic process (e.g., human operators), and services that model stateful servers.
Let S = hO; P ; D0i be a SGDAP where O = hR; T ; Mi and P = hF ; A; i. The semantics of S is defined in terms of a possibly infinite transition system (TS), which represents all possible computations that the process component can do over the data starting from D0. We start by defining the semantics of action execution. Let be an action in A of the form (p~) : fe1; : : : ; eng with effects ei = q + i ^ Q i instance D using a substitution be a substitution of p~ with values in V
. The evaluation of the effects of is captured by the following function:
Ei, and let on a database DO(D; ; ) = Sqi+^Qi
Eiin
S 2ANS((qi+^Qi ) ;D) Ei which returns a database instance made up of values in V and Skolem terms representing service calls. We denote with CALLS(DO(D; ; )) such service calls, and with
: EVALS(D; ; ) = f j : CALLS(DO(D; ; )) ! V is a total functiong:
D by the application of action using substitution if D0 = DO(D; ; ) , where 2 EVALS(D; ; ).
Relational Layer Transition System (RTS). Let S = hO; P; D0i be a SGDAP with O = hR; T ; Mi. The RTS SR of S is formally defined as hR; ; s0; db; )i, where is a (possibly infinite) set of states, s0 is the initial state, db is a total function from states in to database instances made up of values in V and conforming to R, and ) is a transition relation. , ) and db are defined by simultaneous induction as the smallest sets such that s0 2 , with db(s0) = D0, and satisfying the following property: Given s 2 , for each condition-action rule Q(p~) 7! (p~) 2 , for each substitution of p~ such that 2 ANS(Q; D), consider every database instance D0 produced from D by the application of using . Then: (i) if there exists s0 2 such that db(s0) = D0, then s ) s0; (ii) otherwise, if O is satisfiable wrt D0, then s0 2 , s ) s0 and db(s0) = D0, where s0 is a fresh state. We observe that the satisfiability check done in the last step of the RTS construction accounts for semantic governance.
Semantic Layer Transition System (STS). Given a SGDAP S with O = hR; T ; Mi ianndthweistehmRaTnStic lSRay=er.hIRn;par;tisc0u;ldabr,; )SSim,tahientSaTinSs thSSe ostfruSctisurae“ovfirtuSRaluinzaatlitoerne”do,fretflheecRtiTnSg that the process component is executed over the relational layer, but it associates each state to a virtual ABox obtained from the application of the mapping M to the database instance associated by SR to the same state. Formally, SS = hT ; ; s0; abox; )i, where abox is a total function from to ABoxes made up of individual objects in C and conforming to T , such that for each s 2 with db(s) = D, abox(s) = M(D). 5
Let S = hO; P; D0i be an SGDAP where O = hR; T ; Mi and P = hF ; A; i. We are
interested in the verification of conceptual temporal properties over S, i.e., properties
that constrain the dynamics of S understood at the semantic layer. Technically, this means
that properties are verified over the SGDAP’s STS SS, combining temporal operators
with queries posed over the ontologies obtained by combining the TBox T with the
AthBeooWxneetosulaossgesioeacsivoaafteridaSSnt,otaotnhfde s-t-cacataellcscuuollfuuss SS[[11.55M]],otoroenpesrepdoeifcciatfihtceeaolmlvyeo,rswtthepeaoddwyoenpratfmuEliCcteQsmosfp[9o]rSSat.lo lqougeicrys
subsuming LTL, PSL, and CTL* [
EQL formulae only support the limited form of quantification 9x 2 C0: , which fact, LC
= hT ; valuation on ; s0; abox; )i be an STS. Let V be a predicate and individual variable , i.e., a mapping from the predicate variables Z to subsets of the states , and from individual variables to constants in ADOM(M(D0)). Then, we assign meaning EQL formulas to subsets of . The extension function ( )VA is defined inductively as: EQL formulas by associating to
and V an extension function ( )VA , which maps LC
EQL we resort to transition systems. Let
is a closed formula, ( )
are interested in the model checking problem, i.e., verify whether a to
LC
LC = fs 2 = V (Z) = = fs 2 = TfE
A ( )V (Q)VA (Z)VA (: )
A
V ( h i ) ( Z: )VA
A
V ( 1 ^ 2)VA
= ( 1)VA \ ( 2)VA (9x 2 C0: )VA = Sf( )VA [x=c] j c 2 ADOM(M(D0))g j ANS(QV; T ; abox(s)) = trueg
A j 9s0: s ) s0 and s0 2 ( )V g
A j ( )v[Z=E];V
Eg
is a convenient, compact notation for W
form of quantification over time [
for simplicity, but actually, with some care, our result can be extended to a more general c2ADOM(M(D0)) [x=c]. We make this assumption LC
EQL property
, we therefore attack the verification problem way: (1) We transform
into a corresponding whose atoms are closed FO queries over R, thus reducing show, again exploiting FOL rewritability in DL-LiteA, that the consistency check used be generated by a purely relational DCDS. (3) We argue that 0 belongs to the dynamic to generate
R can be rewritten as denial constraints over R S . This means that
Z:((8s:[Student(s)] ! [Graduated(s)]) _ [ ]Z), which says that every evolution of the system 6
LC
the STS and RTS of S. The main issue to be tackled is that
infinite-state, and their verification undecidable. In [
S S S and
S R are in general holds for the SGDAP S
. This problem is defined as checking whether s0 2 ( ) S , for the verification of Data-Centric Dynamic Systems (DCDSs) have been extensively studied. DCDSs are tightly related to SGDAPs, with some key differences in the data component: (i) the process component is identical in the two frameworks; (ii) DCDSs are only equipped with a relational layer, i.e., no ontology nor mapping are specified; (iii) while SGDAPs define constraints over the data at the semantic layer, DCDSs are equipped with denial constraints posed directly over the database schema. Given a
EQL properties can be effectively verified over SGDAPs. Let S = EhQOL; Pdy;nDam0iicbepraonpSeGrtyDAspPecwifiheedreoOver=thheRT;T, ;aMnd ileatnd P = hF ; A; i. Let a LC S and R respectively be
be LC
EQL closed formula
S = tu S = S j
0, i.e., a S = S j to
R = S j in the following
0. (2) We ΥSS A0
M ΥR D0
S
S0
S0 A1
S1
S3
S2 Semantic Transition System M M M D1 S1
S3 A2 A3
D2 D3
S2 Relational Transition System |= Φ |= Φ Φ = unfold(rew(Φ, T ), M) D1 D0
S0
S1
S3
D2 D3
S2 Abstract Transition System |= Φ
Fig. 2. Verification of dynamic LC
property language investigated in [
of the dynamic part and of the embedded ECQs. Since the dynamics of an SGDAP is completely determined at the relational layer, the dynamic part is maintained unaltered.
wrt the TBox T , denoted by r = REW( ; T ), is done by replacing each embedded
Example 5. Consider the LECQL property introduced in Example 1. The rewriting of described in Example 4, together with the TBox T wrt T produces r = REW( ; T ), which is: Z:(8s:[Student(s) _ Bachelor(s) _ Master(s) _ MNum(s; )] ! [Graduated(s)]) _ [ ]Z tu Before unfolding the rewritten dynamic property r we translate each subformula of the form 9x 2 C0: into the equivalent form Wc2ADOM(M(D0)) [x=c]. This means that when such a form of quantification is used, the initial ABox must be materialized in order to compute the initial active domain of the semantic layer. We then extend the UNFOLD() function defined in Section 2 to unfold a LECQL dynamic property over the semantic layer into a corresponding property over the relational layer. As for the rewriting, the temporal structure is maintained unaltered, reflecting that the dynamics of SGDAPs is determined at the relational layer. For what concerns the ECQs embedded in the property, the interesting case to be discussed is the one of (existential) quantification: UNFOLD(9x:'; M) = 9x:UNFOLD('; M) _
W(f=n)2FS(M) 9x1; : : : ; xn:UNFOLD('[x=f (x1; : : : ; xn)]; M) where FS(M) is the set of function symbols contained in M. This unfolding reflects that quantification over individuals at the semantic layer must be properly rephrased as a corresponding quantification over those values in the relational layer that could lead to produce such individuals through the application of M. This is done by unfolding 9x:' into a disjunction of formulae, where: (i) the first formula corresponds to 9x:' itself, and is used to tackle the case in which x appears in the range of an attribute, which is in fact a value; (ii) Each of the other formulae is obtained from ' by replacing x with one of the possible variable terms produced by M, and quantifying over the existence of values used to construct the corresponding object term.
EQL property r of Example 5, together with the mapping M defined in Example 1. We get that UNFOLD( r; M) corresponds to:
Z: 8x1; x2; x3:AUXm3 (x1; x2; x3; ) ! AUXm5 (x1; x2; x3) _ [ ]Z where AUXm3 (name; surname; type; id) and AUXm5 (name; surname; type) represent the auxiliary view predicates of mapping assertions m3 and m5 respectively, whose defining queries are the SQL queries in the left-hand side of the mapping assertion themselves. When unfolding the UCQ Student(stu1(x1; x2; x3)) _ Bachelor(stu1(x1; x2; x3)) _ Master(stu1(x1; x2; x3)) _
Reduction to Data-Centric Dynamic Systems. The connection between SGDAPs
and DCDSs is straightforward (see [
for the DCDS SREL following the definition in [
SREL DCDS, where
SREL DCDS is the RTS constructed
a
LC over the corresponding DCDS. In fact,
EQL property over a SGDAP can be reduced to the verification of a
contained in the fragments of FO
-calculus studied for DCDSs in [
LA and
forms of FO quantification across states, and therefore they clearly support FO sentences.
Let S = hO; P; D0i be a SGDAP with O = hR; T ; Mi, STS hR; ; s0; db; )i. We say that
S = S j belongs to
LP ), (iii) S R is state-bounded if there exists a bound b such
EQL property, and let 0 = be a
LC can be reduced to
S R can be generated by a DCDS
R S j = 0, (ii) 0 S = S j
S
with nondeterministic services, we can reuse the decidability results presented in [
R is state bounded. Verification can in this case be reduced to conventional finite-state model checking. Example 7. Consider the SGDAP S = hO; P; D0i, where O is the OBDA system defined in Example 1, P the process component defined in Example 3. It is easy to see that the resulting
tuples from the TRANSF M table to the ENROLLED one, or copy tuples from the ENROLLED
tive Project ACSI (Artifact-Centric Service Interoperation), funded by the EU under FP7