In the context of veri cation of data-aware processes, a formal approach based on satis ability modulo theories (SMT) has been considered to verify parameterised safety properties of so-called artifactcentric systems. This approach requires a combination of model-theoretic notions and algorithmic techniques based on backward reachability. We introduce here a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs), where, instead of managing a database, we operate over a description logic (DL) ontology expressed in (a slight extension of) RDFS. This DL, enjoying suitable model-theoretic properties, allows us to de ne DL-based SASs to which backward reachability can still be applied, leading to decidability in PSpace of the corresponding safety problems.
Verifying and reasoning about dynamic systems that integrate processes and
data is a long-standing challenge that attracted considerable attention, and that
led to a ourishing series of results, within business process management [
In this paper, we study for the rst time semantic artifact systems where the read-only database is substituted by a Description Logic ontology, which stores background, incomplete information about the artifacts. In this setting, two possible notions of parameterisation may be studied: one where the evolution of the system is veri ed against all possible choices for the ABox, another where veri cation is against all possible models of a xed ABox. In this work, we adopt the latter hypothesis, and thus verify whether the artifact system enjoys desired properties irrespectively of how the information explicitly provided by the ABox is completed through the TBox assertions.
More in detail, we consider an extensively studied, basic model of such
artifact-centric systems, called simple artifact system (SAS ) in [
In spirit, our approach is reminiscent of previous works studying the
verication of dynamic systems (in particular, Golog programs) operating over a
DL ontology, such as [
Full details are provided in the extended version of this paper [
In this section, we rst recall the syntax and semantics of rst-order logic (FO).
We then de ne the syntax of the DL RDFS+ considered in this paper, which is a
slight extension of RDFS [
The alphabet of rst-order logic (FO ) consists of: countably in nite and pairwise disjoint sets NP of predicate symbols (with ar(P ) 2 N being the arity of P 2 NP), NF of function symbols (with ar(f ) 2 N being the arity of f 2 NF), NI of individual symbols (or individual names ), and Var of variables; the equality symbol `='; the Boolean operators `:' and `^'; and the existential quanti er `9'. An (FO ) formula is an expression ' ::= P (t) j s = t j :' j (' ^ ') j 9x', where x 2 Var, P 2 NP, s, t are terms, and t = (t1; : : : ; tar(P )) is a (possibly empty) tuple of terms, where terms are de ned inductively as follows: t ::= x j a j f (t), where x 2 Var, a 2 NI, f 2 NF, and t = (t1; : : : ; tar(f)). A formula of the form P (t) is called an atom, and a literal has the form P (t) or :P (t). We adopt the usual abbreviations and conventions: in particular, ' _ = :(:' ^ : ) and 8x' = :9x:', where 8 is the universal quanti er. We write '(x) to indicate that the free variables (de ned as usual) of ' are included in x, and we write '(a) for the formula obtained from '(x) by substituting a to x. Similar notions and notation are adopted for terms. A sentence is de ned as a formula without free variables, while we call quanti er-free a formula without any occurrence of existential or universal quanti ers. A formula is existential if it has the form 9x'(x), where ' is a quanti er-free formula, and it is universal if it has the form 8x'(x), where ' is quanti er-free. A (FO ) theory T is a set of FO sentences, and T is said to be universal if every ' 2 T is universal. A signature is a subset of NP [ NF [ NI. For a set of formulas, the signature of , denoted , is the set of predicate, function, and individual symbols occurring in . Given a signature , we say that is a set of -formulas if = (we will use -formula, -theory, etc., in an analogous way).
An (FO ) interpretation is a pair I = ( I ; I ), where I is a non-empty set, called domain of I, and I is an interpretation function such that: P I ( I )ar(P ), for every P 2 NP; f I : ( I )ar(f) ! I , for every f 2 NF; and aI 2 I , for every a 2 NI. An assignment in I is a function a : Var ! I . We de ne the value of a term t in I under a as follows: a(t) = a(x), if t = x; a(t) = aI , if t = a 2 NI; and a(t) = f I (a(t)), if t = f (t), where f 2 NF and, for an m-tuple t = (t1; : : : ; tm) of terms, we set a(t) = (a(t1); : : : ; a(tm)). The notion of a formula ' being satis ed in an interpretation I under an assignment a, or of I being a model of ' under a, written I j=a ', is inductively de ned as: I j=a P (t) i I j=a s = t i I j=a : i I j=a ^ i I j=a 9x i a(t) 2 P I ; a(s) = a(t); not I j=a ; I j=a and I j=a ;
I j=a0 for some a0 that can di er from a on x: For a formula '(x), we write I j= '[d] in place of I j=a '(x), with a(x) = d. We say that a set of formulas is satis ed in an interpretation I under an assignment a, or that I is a model of under a, written I j=a , if I j=a ', for every ' 2 (we refer to a singleton = f'g simply as '). For a sentence ', the satisfaction of ' in I under a does not depend on a, thus we write I j= ' in place of I j=a ', and we say that ' is satis ed in I. For a theory T , we say that T is satis ed in an interpretation I (or that I is a model of T ), written I j= T , if every sentence of T is satis ed in I. A formula ' is satis able w.r.t. T (or T -satis able) if there exist an interpretation I and an assignment a in I such that I j= T and I j=a '. Moreover, we say that T logically implies a formula ', or that ' is a logical consequence of T , written T j= ', if, for every interpretation I and every assignment a in I, I j= T implies that I j=a '. Finally, formulas ', are equivalent w.r.t. T (or T -equivalent ) if T j= ' $ . 2.2
Let NC, NR, and NI be countably in nite and pairwise disjoint sets of concept, role, and individual names, respectively (with NC [ NR NP, i.e., concept and role names are predicate symbols, with arity 1 and 2, respectively).
The DL we consider here is an extension of RDFS [
In RDFS+ , concepts C and roles R are de ned according to the grammar R ::= P j P ;
C ::= A1 u u An j 9R:> j 9R:A; where P 2 NR, n 1, and A; A1; : : : ; An 2 NC.
A concept inclusion (CI) has the form C v A or C v :A, and a role inclusion (RI) has the form R v R0 or R v :R0, where C is an RDFS+ concept, A 2 NC, and R, R0 are roles. An RDFS+ TBox T is a nite set of CIs and RIs. An assertion has the form A(a), :A(a), P (a; b), :P (a; b), (a = b), or :(a = b), where A 2 NC, P 2 NR, and a; b 2 NI. An ABox A is a nite set of assertions. (We point out that in an ABox we allow for negated assertions, which is a feature that is not always supported in DLs.) An RDFS+ ontology O is a pair (T ; A), where T is a TBox and A is an ABox.
We observe that RDFS+ is incomparable in expressive power with the DLs
of the popular DL-Lite family [
Example 1. To represent part of the domain knowledge on job hiring processes for university personnel, we de ne the RDFS+ ontology O = (T ; A), where T consists of the following concept inclusions:
while A, which stores data on available job positions, contains the assertions AcademicPosition(professor123); AcademicPosition(researcher123);
AdminPosition(secretary123); AdminPosition(secretary456): Moreover, we assume that A contains all the assertions of the form :A(u), :P (u; a) and :P (a; u), for a distinguished individual name u 2 NI and every A; P; a 2 O, so that u can be used to represent an unde ned value. The CIs of T formalise the following facts: there are both academic and administrative job positions and these are disjoint; users and job positions are disjoint; appliesFor relates users to job positions; to be suitable for something one has to be a user that is positively evaluated; the range of suitableFor is included in the extension of JobPositions; an eligible user is de ned as a graduate user. /
We de ne now the standard translation from RDFS+ expressions to FO formulas, which maps concepts to FO formulas with one free variable, and roles to FO formulas with two free variables. Speci cally, the translation T generates formulas that contain just two variables x; y 2 Var, and is de ned as follows: T(A1 u u An) = A1(x) ^
T(P ) = P (x; y); T(9R:>) = 9yT(R);
T(:A) = :T(A); ^ An(x);
T(P ) = P (y; x); T(9R:A) = 9y(T(R) ^ A(y));
T(:R) = :T(R);
where A; A1; : : : ; An are unary predicates and P is a binary predicate. Moreover,
we map CIs and RIs into universal FO sentences in the following way:
T(C v D) = 8x(T(C) ! T(D));
T(R v S) = 8x8y(T(R) ! T(S));
where D stands for either A or :A, and S stands for either R0 or :R0. We
also set T(T ) = S 2T fT( )g. Assertions are (identically) mapped into FO
literals without free variables (i.e., ground ), as T( ) = , and we set T(A) =
S 2AfT( )g. Finally, T(O) = T(T ) [ T(A). It is easy to see that the set of FO
sentences obtained as the translation T(O) of an RDFS+ ontology O, can be
equivalently rewritten into a universal Horn theory [
The semantics for RDFS+ expressions can be given in terms of their FO
translation [
Moreover, given a CI, RI, assertion, TBox, ABox, or ontology , we say that is satis ed in I (or that I is a model of ), written I j= , i I j= T( ). Given an ontology O and (a concept, role, CI, RI, or assertion mapped, via its FO translation, into) an FO formula ', we say that ' is satis able w.r.t. O (or O-satis able) if there exists a model I of O that satis es ' under some assignment in I. Finally, we say that O logically implies an FO formula ', or that ' is a logical consequence of O, written O j= ', if, for every model I of O and every assignment a in I, we have that I satis es ' under a. 3
In this section, we prove the model-theoretic properties that will be used later
on to develop our veri cation machinery. Speci cally, we show here that the
standard translation of the RDFS+ ontologies introduced in the previous section
admits model completion, and has the constraint satis ability problem decidable.
These properties will allow us, in the subsequent sections, to verify suitably
de ned DL-based data-aware processes by employing a variant of the SMT-based
backward reachability procedure introduced in [
A formula that is a conjunction of -literals is called a -constraint. Given a
-theory T , we de ne the constraint satis ability problem for T as follows: given
a formula 9y'(x; y), where '(x; y) is a -constraint, decide whether 9y'(x; y)
is satis able w.r.t. T . A theory T has quanti er elimination i , for every T
formula '(x), there exists a quanti er-free formula (x) such that T j= '(x) $
(x). Finally, we will use the following de nition of model completion, which
is restricted to cover the case of universal theories (the ones considered in this
work) and that is nonetheless known to be equivalent (for universal theories) to
the usual one from model theory [
We now state the main technical result of the section. Theorem 2. Given an RDFS+ ontology O, T(O) is a nite universal FO theory that (i) has a decidable constraint satis ability problem, and (ii) admits a model completion.
Proof (Sketch). To prove Point (i), we reduce to RDFS+ (seen as a fragment of
ALCHI, [
Properties (i) and (ii) from Theorem 2 are in line with the foundational
framework of [
In this section, we present our main contributions. We rst de ne our model,
called RDFS+ -based simple artifact systems, or RDFS+ -SASs for short, to
formalise data-aware processes under RDFS+ ontologies. These systems are a
variant of the artifact-centric systems studied in [
We rst require the following preliminary notions. For an RDFS+ ontology O, an O-partition is a nite set P = f 1(x); : : : ; n(x)g of O-literals such that O j= 8x Win=1 i(x) ^ 8x Vi6=j :( i(x) ^ j (x)). Given an ontology O, an Opartition P = f 1(x); : : : ; n(x)g, and O-terms t(x) = (t1(x); : : : ; tn(x)), (the value of) a case-de ned function F based on P and t, for a fresh function symbol
F 2 NF, is de ned as follows: for every model I of O, every assignment a in I, and every tuple x of variables, a(F (x)) = a(ti(x)), if I j=a i(x).
In order to introduce veri cation problems in a symbolic setting, one rst has to specify which formulas are used to represent (i) the sets of states, (ii) the system initialisations, and (iii) the system evolution. To capture these aspects, we provide the following de nitions.
An RDFS+ -based simple artifact system (RDFS+ -SAS) is a tuple
S = (O; x; (x); Sjm=1f j (x; x0)g); where m 2 N, and { O = (T ; A) is an RDFS+ ontology; { x = (x1; : : : ; xn) is a tuple of variables, called artifact variables, and x0 is a tuple of variables that are renamed copies of variables in x; { (x) = Vin=1 xi = ai, with ai 2 NI, is an initial state formula; { j (x; x0) = 9y( j (x; y) ^ Vin=1 x0i = Fij (x; y)), for 1 j m, is a transition formula, where j (x; y) is a conjunction of O-literals called guard of j , and x0i = Fij (x; y), where each Fij is a case-de ned function based on some O-partition and list of O-terms, is an update of j .
Given an RDFS+ ontology O, we call state ( O-)formula a quanti er-free O-formula '(x). A state formula constrains the content of the artifact variables characterising the current states of the systems. Notice that a state formula can represent a (possibly in nite) set of states, because of the presence of (possibly in nitely many) di erent elements in a model of the ontology O. A safety formula for S is a state O-formula (x), used to describe the undesired states of the system. We say that S is safe w.r.t. (x) if there does not exist k 0 and a formula of the form (x0) ^ j0 (x0; x1) ^ ^ jk 1 (xk 1; xk) ^ (xk); (?) that is satis able w.r.t. O, where 1 j0; : : : ; jk 1 m and each xh, with 0 h k, is a tuple of variables that are renamed copies of variables in x. The safety problem for S is the following decision problem: given a safety formula (x) for S, decide whether S is safe w.r.t. (x). This veri cation problem is parametric on the models of a xed RDFS+ ontology, since safety is assessed irrespectively of the choice of such a model. This implies that, when the system is safe, it is so for every execution of the process under every possible model (which in principle are in nitely many) of the given ontology.
Example 4. We develop a simpli ed job hiring process for university personnel based on the domain knowledge formalised in Example 1. Each application is created using a dedicated website portal, where users that are potentially interested in applying need to register in advance. When a registered user decides to apply, the data created by this single application do not have to be stored persistently and thus can be maintained just by using artifact variables (described below) that can interact with the knowledge base. All these variables are initialised with an unde ned value u. In the rst transition of the system, an application is created by a registered user, which falls into the extension of the concept User: the information about this user is then stored in the artifact variable xapplicant. At this point, the application website asks the user whether they hold a university degree: in case of an a ermative answer, the website accepts the user as eligible, the information about the user is stored using xapplicant and the process can progress. Then, the user picks up a job position (assigned to xjob) and applies for it. The following steps of the process involve the evaluation of the application: for both academic and administrative positions, if the eligible candidate is suitable for the chosen position, they are declared winner (assigned to xwinner), otherwise they are declared loser (assigned to xloser). To formalise this process, we de ne the RDFS+ -SAS S = (O; x; (x); Sj7=1f j (x; x0)g) so that: { the ontology O is the RDFS+ ontology given in Example 1; { the artifact variables are x = (xapplicant; xjob; xeligible; xwinner; xloser); { the initial state formula is
= (xapplicant = u) ^ (xjob = u) ^ (xeligible = u) ^ (xwinner = u) ^ (xloser = u); { the transition formulas are 1 = 9y1(User(y1) ^ x0applicant = y1); 2 = EligibleUser(xapplicant) ^ x0eligible = xapplicant; 3 = 9z1(JobPosition(z1) ^ appliesFor(xeligible; z1) ^ xj0ob = z1); 4 = AcademicPosition(xjob) ^ suitableFor(xeligible; xjob) ^ x0winner = xeligible; 5 = AdminPosition(xjob) ^ suitableFor(xeligible; xjob) ^ x0winner = xeligible; 6 = AcademicPosition(xjob) ^ :suitableFor(xeligible; xjob) ^ xl0oser = xeligible; 7 = AdminPosition(xjob) ^ :suitableFor(xeligible; xjob) ^ xl0oser = xeligible: An undesired situation of the system is the one where an applicant registered user is declared winner even if they were not eligible. This situation is formally described by the following safety formula for S: = User(xwinner) ^ :EligibleUser(xwinner): / 4.2
Backward Search for RDFS+ -SASs Algorithm 1 shows the SMT-based backward reachability procedure (or backward search) for handling the safety problem for an RDFS+ -SAS S. An integral part of the algorithm is to compute symbolic preimages (Line 5). The intuition behind the algorithm is to execute a loop where, starting from the undesired states of the system (described by the safety formula (x)), the state space of the system is explored backward : in every iteration of the while loop (Line 2), the current set of states is regressed through transitions thanks to the preimage computation. For that purpose, for any (z; z0) and (z) (where z0 are renamed copies of z), we de ne := Whm=1 h and Pre( ; ) as the formula 9z0( (z; z0) ^ (z0)). Let (x) be a state formula, describing the state of the artifact variables x. The preimage of the set of states described by the formula (x) is the set of states described by Pre( ; ) (notice that, when = W ^, then Pre( ; ) = W Pre(^; )). We recall that a state formula is a quanti er-free O-formula. Unfortunately, because of
Algorithm 1: SMT-based backward reachability procedure
the presence of the existentially quanti ed variables y in , Pre( ; ) is not a
state formula, in general. As stated in [
QE(T (O) ; ) in Line 6 is a subprocedure that implements the quanti er elimination algorithm of T (O) and that converts the preimage Pre( ; ) of a state formula into a state formula (equivalent to it modulo the axioms of T (O) ), so as to guarantee the regressability of the procedure: this conversion is possible since T (O) eliminates from h the existentially quanti ed variables y. Backward search computes iterated preimages of the safety formula , until a xpoint is reached (in that case, S is safe w.r.t. ) or until a set intersecting the initial states (i.e., satisfying ) is found (in that case, S is unsafe w.r.t. ). Inclusion (Line 2) and disjointness (Line 3) tests can be discharged via proof obligations to be handled by SMT solvers. The xpoint is reached when the test in Line 2 returns unsat : the preimage of the set of the current states is included in the set of states reached by the backward search so far (represented as the iterated application of preimages to the safety formula ). The test at Line 3 is satis able when the states visited so far by the backward search includes a possible initial state (i.e., a state satisfying ). If this is the case, then S is unsafe w.r.t. . Together with the unsafe outcome, the algorithm also returns an unsafe trace of the form (?), explicitly witnessing the sequence of transitions h that, starting from the initial con gurations, lead the system to a set of states satisfying the undesired conditions described by (x).
Theorem 5. Backward search (Algorithm 1) is correct for detecting whether an RDFS+ -SAS S is safe w.r.t. (x).
Proof (Sketch). First, we require the following claim, which follows immediately from the de nitions. Claim 1. For every safety formula (x) for S and every k 0, a formula # of the form (?) is satis able w.r.t. O i # is satis able w.r.t. T (O).
Then, we need to show that, instead of considering satis ability of formulas of the form (?) in models of T (O), we can concentrate on satis ability w.r.t. T (O) (T (O) exists thanks to Property (ii) of Theorem 2). Then, by exploiting the algorithm for quanti er elimination in T (O) described in Remark 3, formulas of the form (?) can be represented via backward search by using quanti er-free formulas. We nally conclude by noticing that safety/unsafety of S w.r.t (x) can be now detected invoking the satis ability tests (which are e ective thanks to Property (i) of Theorem 2) over those quanti er-free formulae.
Backward search for generic artifact systems is not guaranteed to
terminate [
Theorem 6. For an RDFS+ ontology O and an RDFS+ -SAS S = (O; x; (x); Sm
j=1f j (x; x0)g), the safety problem for S is decidable in PSpace in the combined size of x, (x) and Sm
j=1f j (x; x0)g.
Proof (Sketch). For every RDFS+ ontology O, there are only nitely many quanti er-free T (O)-formulas, up to T (O)-equivalence, that can be built out of a nite set of variables x. Thanks to the availability of the quanti er elimination procedure QE(T (O) ; '), the overall number of variables in ' is never increased. This implies that globally there are only nitely many quanti er-free
T (O)-formulas that Algorithm 1 needs to analyse. Hence, Algorithm 1 terminates. Concerning complexity, we rst note that the translation T (O) requires polynomial time. Then, we need to eliminate the occurrences of case-de ned functions (creating an equivalent SAS whose size is polynomial in the size of the original one), and to modify Algorithm 1 by making it nondeterministic with an NPSpace complexity. The claim follows by applying Savitch's Theorem.
We observe that Algorithm 1 is not yet implemented in the state-of-the-art
model checker MCMT (Model Checker Modulo Theories [
We have studied the problem of veri cation of data-aware processes under RDFS+ ontologies, where the process component can interact with a knowledge base speci ed by means of the DL RDFS+ , underpinning the RDFS constructs. We addressed this problem by introducing a suitable model of DL-based artifactcentric systems, called RDFS+ -based SASs, and by leveraging the SMT-based version of the backward reachability procedure, which is a well-known technique to employ for verifying systems of this kind. Speci cally, we showed that this procedure is a full decision procedure for detecting safety of RDFS+ -based SASs, and we also provided a PSpace complexity upper bound.
This work opens several directions for future work. First, we notice that the
choice of RDFS+ ontologies is not intrinsic to our approach. Indeed, motivated
by conceptual modelling and data integration issues in OBDA applications, we
are currently working on the DL-Lite family of DLs, to de ne suitable
DLLite-based SASs with analogous decidability and complexity results. The main
di erence we have to account for is that, for a DL-Lite ontology O, we have an
equisatis able (but not equivalent) translation into a universal one-variable FO
sentence T (O), and Claim 1 in the proof of Theorem 5 has to be modi ed to show
that a trace # is satis able w.r.t. O i a suitably translated trace #^ is satis able
w.r.t. T (O). In general, nonetheless, we point out that any DL satisfying the
two conditions stated in Theorem 2 can be chosen for our purposes, and that
the same theoretical guarantees can be obtained over the SMT-based backward
reachability procedure. As future work, we thus intend to introduce a more
general framework for DL-based SASs that is able to account for di erent DLs.
We also intend to extend the results obtained here to more sophisticated
artifactcentric models, such as the relational artifact systems (RASs) studied in [
This research has been partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation, by the Italian Basic Research (PRIN) project HOPE, by the EU H2020 project INODE (grant agreement 863410) by the CHIST-ERA project PACMEL, by the project IDEE (FESR1133) funded by the Eur. Reg. Development Fund (ERDF) Investment for Growth and Jobs Programme 20142020, and by the Free University of Bozen-Bolzano through the projects KGID, GeoVKG, STyLoLa, VERBA and MENS.