{'fraction_non_alphanumeric': 0.06252406887825274, 'fraction_numerical': 0.006656764042471255, 'mean_word_length': 3.937525465163656, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)

In the context of verification of data-aware processes (DAPs), a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety properties of so-called artifact-centric 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 define DL-based SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.


Introduction
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 flourishing series of results, within business process management [29,9,20] and data management [31,8,4,17,18]. Among the several conceptual models studied in this area, data-centric systems and in particular artifact-centric systems have been brought forward as a principled approach where relevant (business) objects are elicited, then defining how actions evolve them throughout their lifecycle [24]. Different formal models have been proposed to capture artifact systems and study their verification [8]. One of the most studied settings considers artifact systems as being composed of: a read-only database storing background information about artifacts that does not change during the evolution of the system; a working memory, used to store data that can be modified in the course of the evolution; and transitions (also called actions or services) that query the read-only database and the working memory and use the retrieved answers to update the working memory. Verification of such systems is particularly challenging, not only because the working memory in general evolves through infinitely many different configurations, but also because the desired verification properties should hold regardless of the specific content of the read-only database, thus calling for a particular form of parameterised verification [15,18,10,11].
In this paper, we study for the first 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 verified against all possible choices for the ABox, another where verification is against all possible models of a fixed 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 [11], where the artifact working memory consists of a fixed set of artifact variables [16,15,11]. On top of this basis, we study the verification of safety properties in the case where the ontology is specified in (a slight extension of) RDFS [6], a schema language for the Semantic Web formalized by the W3C, and we make use of the ontology signature to express the transitions that update the working memory. For this setting, we show that we can decide safety properties in PSpace by relying on an SMT-based backward reachability procedure.
In spirit, our approach is reminiscent of previous works studying the verification of dynamic systems (in particular, Golog programs) operating over a DL ontology, such as [14,33]. In fact, both in their settings and ours, the dynamic system evolves each model of the ontology, and verification properties are assessed over all the resulting evolutions. This is radically different from approaches where the ABox itself is evolved by the process, with an execution semantics following Levesque's functional approach, in which query entailment over the current state is used to compute the successor states [3,5]. However, we differ from [14,33] in that our goal is not only to derive foundational results, but also to transfer such results into practical algorithms and thus obtain a model that is readily implementable by relying on a state-of-the-art SMT-based model checker such as MCMT [22]. As customary in the formal literature on artifact-centric systems, our approach is based on actions that manipulate the artifact variables, coupled with condition-action rules that declaratively define which actions are currently executable, and with which parameters. Alternative choices could be seamlessly taken, by adapting approaches that rely on an explicit description of the control-flow, e.g., based on state machines [26] or Petri nets interpreted with interleaving semantics [20,28]. This paper is the extended version of [12]. All the detailed proofs can be found in the appendix.

Preliminaries
In this section, we first recall the syntax and semantics of first-order logic (FO). We then define the syntax of the DL RDFS + considered in this paper, which is a slight extension of RDFS [6]. Its semantics is provided by means of the standard translation, mapping RDFS + ontologies into equivalent sets of FO formulas.

First-Order Logic Preliminaries
The alphabet of first-order logic (FO ) consists of: countably infinite and pairwise disjoint sets N P of predicate symbols (with ar(P ) ∈ N being the arity of P ∈ N P ), N F of function symbols (with ar(f ) ∈ N being the arity of f ∈ N F ), N I of individual symbols (or individual names), and Var of variables; the equality symbol '='; the Boolean operators '¬' and '∧'; and the existential quantifier '∃'. An (FO ) formula is an expression ϕ ::= P (t) | s = t | ¬ϕ | (ϕ ∧ ϕ) | ∃xϕ, where x ∈ Var, P ∈ N P , s, t are terms, and t = (t 1 , . . . , t ar(P ) ) is a (possibly empty) tuple of terms, where terms are defined inductively as follows: t ::= x | a | f (t), where x ∈ Var, a ∈ N I , f ∈ N F , and t = (t 1 , . . . , t ar(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 ∀xϕ = ¬∃x¬ϕ, where ∀ is the universal quantifier. We write ϕ(x) to indicate that the free variables (defined 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 defined as a formula without free variables, while we call quantifier-free a formula without any occurrence of existential or universal quantifiers. A formula is existential if it has the form ∃xϕ(x), where ϕ is a quantifier-free formula, and it is universal if it has the form ∀xϕ(x), where ϕ is quantifier-free. A (FO ) theory T is a set of FO sentences, and T is said to be universal if every ϕ ∈ T is universal. A signature Σ is a subset of N P ∪ N F ∪ N I . 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 ∈ NP; f I : (∆ I ) ar(f ) −→ ∆ I , for every f ∈ N F ; and a I ∈ ∆ I , for every a ∈ N I . An assignment in I is a function a : Var −→ ∆ I . We define the value of a term t in I under a as follows: a(t) = a(x), if t = x; a(t) = a I , if t = a ∈ N I ; and a(t) = f I (a(t)), if t = f (t), where f ∈ N F and, for an m-tuple t = (t 1 , . . . , t m ) of terms, we set a(t) = (a(t 1 ), . . . , a(t m )). The notion of a formula ϕ being satisfied in an interpretation I under an assignment a, or of I being a model of ϕ under a, written I |= a ϕ, is inductively defined as: iff not I |= a ψ, I |= a ψ ∧ χ iff I |= a ψ and I |= a χ, I |= a ∃xψ iff I |= a ′ ψ for some a ′ that can differ from a on x.
For a formula ϕ(x), we write I |= ϕ[d] in place of I |= a ϕ(x), with a(x) = d. We say that a set Γ of formulas is satisfied in an interpretation I under an assignment a, or that I is a model of Γ under a, written I |= a Γ , if I |= a ϕ, for every ϕ ∈ Γ (we refer to a singleton Γ = {ϕ} simply as ϕ). For a sentence ϕ, the satisfaction of ϕ in I under a does not depend on a, thus we write I |= ϕ in place of I |= a ϕ, and we say that ϕ is satisfied in I. For a theory T , we say that T is satisfied in an interpretation I (or that I is a model of T ), written I |= T , if every sentence of T is satisfied in I. A formula ϕ is satisfiable w.r.t. T (or T -satisfiable) if there exist an interpretation I and an assignment a in I such that I |= T and I |= a ϕ. Moreover, we say that T logically implies a formula ϕ, or that ϕ is a logical consequence of T , written T |= ϕ, if, for every interpretation I and every assignment a in I, I |= T implies that I |= a ϕ. Finally, formulas ϕ, ψ are equivalent w.r.t. T (or T -equivalent ) if T |= ϕ ↔ ψ.

Description Logics Preliminaries
Let N C , N R , and N I be countably infinite and pairwise disjoint sets of concept, role, and individual names, respectively (with N C ∪ N R ⊆ N P , 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 [6] with disjointness between concepts and roles, conjunction and (one-level) qualified existential quantification on the left-hand side of inclusions, and inclusion of direct and inverse roles. We denote such DL RDFS + , and we define it below.
In RDFS + , concepts C and roles R are defined according to the grammar R ::= P | P − , C :: where P ∈ N R , n ≥ 1, and A, A 1 , . . . , A n ∈ N C . A concept inclusion (CI) has the form C ⊑ A or C ⊑ ¬A, and a role inclusion (RI) has the form R ⊑ R ′ or R ⊑ ¬R ′ , where C is an RDFS + concept, A ∈ N C , and R, R ′ are roles. An RDFS + TBox T is a finite 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 ∈ N C , P ∈ N R , and a, b ∈ N I . An ABox A is a finite 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 [7,2]. Indeed, while DL-Lite allows for the use of existential quantification on the right-hand side of CIs, these are ruled out in RDFS + . On the other hand, in RDFS + one can locally type the second component of a role through the use of qualified existential quantification on the left-hand side of CIs, while this is not possible in DL-Lite. As we will see later, differently from what happens for DL-Lite, the FO translation of an RDFS + ontology is a universal theory. 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 ∈ N I and every A, P, a ∈ Σ O , so that u can be used to represent an undefined 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 defined as a graduate user. ⊳ We define 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. Specifically, the translation T generates formulas that contain just two variables x, y ∈ Var, and is defined as follows: where A, A 1 , . . . , A n are unary predicates and P is a binary predicate. Moreover, we map CIs and RIs into universal FO sentences in the following way: where D stands for either A or ¬A, and S stands for either R ′ or ¬R ′ . We also set T(T ) = β∈T {T(β)}. Assertions α are (identically) mapped into FO literals without free variables (i.e., ground ), as T(α) = α, and we set 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 [25,23]. Such a theory, which we identify with T (O), can be obtained from T (O) by simply putting formulas into prenex normal form.
The semantics for RDFS + expressions can be given in terms of their FO translation [25]. For an interpretation I = (∆ I , · I ) and a concept C, we define the extension of C in I as Similarly, for a role R, we define its extension in I as We say that C and R are satisfied in I if C I = ∅ and R I = ∅, respectively.
Moreover, given a CI, RI, assertion, TBox, ABox, or ontology Γ , we say that Γ is satisfied in I (or that I is a model of Γ ), written I |= Γ , iff I |= T(Γ

Basic Model-Theoretic Properties
In this section, we prove the model-theoretic properties that will be used later on to develop our verification machinery. Specifically, we show here that the standard translation of the RDFS + ontologies introduced in the previous section admits model completion, and has the constraint satisfiability problem decidable. These properties will allow us, in the subsequent sections, to verify suitably defined DL-based data-aware processes by employing a variant of the SMT-based backward reachability procedure introduced in [10]. To present our results, we require the following preliminary notions.
A formula that is a conjunction of Σ-literals is called a Σ-constraint. Given a Σ-theory T , we define the constraint satisfiability problem for T as follows: given a formula ∃yϕ(x, y), where ϕ(x, y) is a Σ-constraint, decide whether ∃yϕ(x, y) is satisfiable w.r.t. T . A theory T has quantifier elimination iff, for every Σ Tformula ϕ(x), there exists a quantifier-free formula ψ(x) such that T |= ϕ(x) ↔ ψ(x). Finally, we will use the following definition 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 [13,19,10]. Let T be a universal Σ-theory and let T * ⊇ T be a further Σ-theory. We say that T * is a model completion of T iff: (i) every Σ-constraint satisfied in some model of T is also satisfied in some model of T * ; (ii) T * has quantifier elimination.
We now state the main technical result of the section. Properties (i) and (ii) from Theorem 2 are in line with the foundational framework of [10,11], where a third property is additionally assumed: the finite model property for constraint satisfiability (see the references for the definition). However, differently from [10,11], this property is not needed anymore for the results of our paper. This is an important difference from [10,11], since the artifact systems studied there require to interact with finite structures (i.e., databases), whereas in the context of the present work we admit that the models of the knowledge base of our artifact systems can be infinite.

Ontology-Based Data-Aware Processes
In this section, we present our main contributions. We first define 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 [10]. RDFS + -SASs read data from a given RDFS + ontology, used to store background information of the system, and manipulate individual variables, called artifact variables, which represent the current state of the process. We then study the parameterised safety problems of such models by adopting a symbolic version [21,11] of the well-known backward reachability procedure [1].

DL-Based Simple Artifact Systems
We first require the following preliminary notions. For an RDFS + ontology O, . . , t n (x)), (the value of) a case-defined function F based on P and t, for a fresh function symbol F ∈ N F , is defined as follows: for every model I of O, every assignment a in I, and every tuple x of variables, a(F (x)) = a(t i (x)), if I |= a κ i (x).
In order to introduce verification problems in a symbolic setting, one first 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 definitions.
An RDFS + -based simple artifact system (RDFS + -SAS) is a tuple where m ∈ N, and is a tuple of variables, called artifact variables, and x ′ is a tuple of variables that are renamed copies of variables in x; that is satisfiable w.r.t. O, where 1 ≤ j 0 , . . . , j k−1 ≤ m and each x h , 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 verification problem is parametric on the models of a fixed 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 infinitely many) of the given ontology.
Example 4. We develop a simplified 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 undefined value u. In the first 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 x applicant . At this point, the application website asks the user whether they hold a university degree: in case of an affermative answer, the website accepts the user as eligible, the information about the user is stored using x applicant and the process can progress. Then, the user picks up a job position (assigned to x job ) 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 x winner ), otherwise they are declared loser (assigned to x loser ). To formalise this process, we define the RDFS 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(x winner ) ∧ ¬EligibleUser(x winner ). ⊳

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, z ′ ) and φ(z) (where z ′ are renamed copies of z), we define τ := m h=1 τ h and Pre(τ, φ) as the formula ∃z ′ (τ (z, z ′ ) ∧ φ(z ′ )). 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 Algorithm 1: SMT-based backward reachability procedure Pre(τ, φ) (notice that, when τ = τ , then Pre(τ, φ) = Pre(τ , φ)). We recall that a state formula is a quantifier-free Σ O -formula. Unfortunately, because of the presence of the existentially quantified variables y in τ , Pre(τ, φ) is not a state formula, in general. As stated in [10,11], if the quantified variables were not eliminated, we would break the regressability of the procedure: indeed, the states reached by computing preimages, intuitively described by Pre(τ, φ), need to be represented by a state formula φ ′ in the new iteration of the while loop. In addition, the increase of the number of variables due to the iteration of the preimage computation would affect the performance of the satisfiability tests described below, in case the loop is executed many times. In order to solve these issues, it is essential to introduce the subprocedure QE(T (O) * , φ) in Line 6.
QE(T (O) * , φ) in Line 6 is a subprocedure that implements the quantifier 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 quantified variables y. Backward search computes iterated preimages of the safety formula ν, until a fixpoint 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 fixpoint 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 satisfiable 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 configurations, lead the system to a set of states satisfying the undesired conditions described by ν(x).
Proof (Sketch). First, we require the following claim, which follows immediately from the definitions. Then, we need to show that, instead of considering satisfiability of formulas of the form (⋆) in models of T (O), we can concentrate on satisfiability w.r.t. T (O) * (T (O) * exists thanks to Property (ii) of Theorem 2). Then, by exploiting the algorithm for quantifier elimination in T (O) * described in Remark 3, formulas of the form (⋆) can be represented via backward search by using quantifier-free formulas. We finally conclude by noticing that safety/unsafety of S w.r.t ν(x) can be now detected invoking the satisfiability tests (which are effective thanks to Property (i) of Theorem 2) over those quantifier-free formulae.
Backward search for generic artifact systems is not guaranteed to terminate [11]. However, in case S is unsafe w.r.t. ν(x), an unsafe trace-which is finite-is found after finitely many iterations of the while loop: hence, in the unsafe case, backward search must terminate. Together with the theorem above, this means that the backward reachability procedure is at least a semi-decision procedure for detecting unsafety of RDFS + -SASs. Nevertheless, we show in the following theorem that, in case of RDFS + -SASs, backward search always terminates: thus, it is a full decision procedure, for which we also provide a PSpace upper bound. , the overall number of variables in ϕ is never increased. This implies that globally there are only finitely many quantifier-free Σ T (O) -formulas that Algorithm 1 needs to analyse. Hence, Algorithm 1 terminates. Concerning complexity, we first note that the translation T (O) requires polynomial time. Then, we need to eliminate the occurrences of case-defined 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 [21]), which is based on SMT solving. Such an implementation, however, can be obtained by extending MCMT with the quantifier elimination algorithm for T (O) * (described in Remark 3), required in Line 6, together with a procedure for RDFS+ ontology satisfiability (seen as a fragment of ALCHI, [30]), required in Lines 2 and 3.

Conclusions
We have studied the problem of verification of data-aware processes under RDFS + ontologies, where the process component can interact with a knowledge base specified 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. Specifically, 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 define suitable DL-Lite-based SASs with analogous decidability and complexity results. The main difference we have to account for is that, for a DL-Lite ontology O, we have an equisatisfiable (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 modified to show that a trace ϑ is satisfiable w.r.t. O iff a suitably translated traceθ is satisfiable 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 different DLs. We also intend to extend the results obtained here to more sophisticated artifactcentric models, such as the relational artifact systems (RASs) studied in [10,11]. Moreover, it could be worth investigating in this setting also properties that go beyond safety, such as liveness and fairness.

Proofs for Section 3
In the following, given a signature Σ, we call a Σ-interpretation an interpretation I = (∆ I , · I ), where the domain of · I is restricted to Σ. Let I and J be Σinterpretations. A Σ-homomorphism (or simply homomorphism) from I to J is a function µ : ∆ I −→ ∆ J , denoted by µ : I −→ J , satisfying the following conditions, for every d in ∆ I : (1) for every individual symbol a ∈ Σ, µ(a I ) = a J ; (2) for every function symbol f ∈ Σ, µ(f I (d)) = f J (µ(d)); (3) for every predicate symbol P ∈ Σ, if d ∈ P I , then µ(d) ∈ P J .
We say that a homomorphism µ : I −→ J is an embedding from I to J if µ is injective and such that: We say that I is a substructure of J , and that J is an extension of I, written I ⊆ J , iff ∆ I ⊆ ∆ J and the identity inclusion i : ∆ I −→ ∆ J is an embedding from I to J .
Theorem 2. Given an RDFS + ontology O, T(O) is a finite universal FO theory that (i) has a decidable constraint satisfiability problem, and (ii) admits a model completion.
Proof. Concerning Property (i), we have that the constraint satisfiability problem for T(O) can be reduced to the RDFS + ontology satisfiability problem, seen as a fragment of ALCHI, for which this problem is known to be decidable [30]. Indeed, let To show Property (ii), we first require the following claim.
Claim. Given a signature Σ without function symbols, every universal Σ-theory T that has the amalgamation property admits a model completion.
By the previous claim, since Σ T (O) does not contain function symbols and T (O) is universal, to prove that T (O) admits a model completion, it is enough to show that T (O) has the amalgamation property. We prove this as follows. Consider Σ T (O) -interpretations I 1 and I 2 that are models of T (O), and let I 0 be a substructure of both I 1 and I 2 that is a model of T (O) (we assume w.l.o.g. that ∆ I1 ∩ ∆ I2 = ∆ I0 ). We define the Σ T (O) -interpretation I = (∆ I , · I ) as follows: Observe that a I = a I1 = a I0 = a I2 . Moreover, if d ∈ P I , where P is n-ary, for n ∈ {1, 2}, then d ∈ (∆ I1 ) n and d ∈ P I1 , or d ∈ (∆ I2 ) n and d ∈ P I2 : this follows from the definition of P I := P I1 ∪P I2 . Clearly, given embeddings µ 1 : I 0 −→ I 1 , (4) ∀x∀y(R 1 (x, y) → R 2 (x, y)); (5) ∀x∀y(R 1 (x, y) → ¬R 2 (x, y)); where: A k ∈ N C , for k ∈ {1, . . . , n}; λ ∈ {B, ¬B}, with B ∈ N C ; R i (x, y) = P i (x, y), if R i = P i , and R i (x, y) = P i (y, x), if R i = P − i , with P i ∈ N R and i ∈ {1, 2}. We now show, reasoning by cases, that for every j ∈ {1, . . . , 5} and every formula ϕ ∈ T (O) of the form (j), I is a model of ϕ.
(1) Given d ∈ ∆ I , suppose that I |= Given that R 2 (x, y) is a literal and I i is embedded in I, we obtain that I |= λ[d], and thus I |= ϕ. The cases with R i = P i (y, x), for i = 1 or i = 2, are analogous. (5) This case is analogous to the previous one, since ¬R 2 (x, y) is a literal and I i is embedded in I.
Thus, we conclude that I |= ϕ, for every ϕ ∈ T (O), i.e., I |= T (O). This completes the proof that I is a T (O)-amalgam of I 1 , I 2 over I 0 , hence T (O) has the amalgamation property. By the claim above, we obtain that T (O) admits a model completion.
Following an analogous argument to the one used in [11,Proposition 3.2], one can also exhibit the algorithm for quantifier elimination in the model completion of T(O): given a formula ∃xϕ(x, y), take the quantifier-free formula ψ(y) as the conjunction of the set of all quantifier-free formulae χ(y) such that ϕ(x, y) → χ(y) is a logical consequences of T(O) (they are clearly finitely many, up to T(O)-equivalence).
Proofs for Section 4 Lemma 7. The safety problem for an RDFS + -SAS S can be reduced to the safety problem for an RDFS + -SAS S ′ (the size of which is polynomial in the size of S) without any occurrence of case-defined functions.
Proof. We first require the following claim.

Claim. For every RDFS
such that: (i) the transition formulas τ ′ j , for 0 ≤ j ≤ m ′ , do not contain any case-defined function; and (ii) for every safety formula ν(x), there exists a formula ϑ k S,ν of the form (⋆) that is satisfiable w.r.t. O, for some k ≥ 0, iff there exists a formula ϑ k ′ S ′ ,ν of the form (⋆) that is satisfiable w.r.t. O, for some k ′ ≥ 0. The construction of S ′ is polynomially long in the size of S (i.e., O(n 2 ), when n is the overall size of S).
Proof of Claim. First, concerning Point (i), we observe that, given an RDFS + ontology O and a formula ϕ containing a case-defined function F (based on some O-partition and list of Σ O -terms), there exists a formula ϕ † not containing any occurrence of F and such that O |= ϕ ↔ ϕ † . Such a formula ϕ † can be obtained from ϕ by substituting every atom α in which F (x) occurs by the disjunction are cased-defined functions based on some O-partitions and lists of Σ O -terms. By substituting each y)) and applying first-order logic transformations, we obtain the formula p which is equivalent to the original τ h (x, x ′ ) in all models of O. Notice that the size of each τ † h,j is clearly O(n), where n is the overall size of the input S, and, since p = O(n), there are O(n 2 ) such τ † h,j . Hence, the size of S ′ is O(n 2 ), as wanted. By taking, for all the relevant 1 ≤ h ≤ m, The statement of the lemma then follows from the previous claim: it is sufficient to notice that, for every safety formula ν(x), there is no k ≥ 0 and no formula ϑ k S,ν of the form (⋆) that is satisfiable w.r.t. O iff there is no k ′ ≥ 0 and no formula ϑ k ′ S ′ ,ν of the form (⋆) that is satisfiable w.r.t. O. This implies that S is safe w.r.t. ν(x) iff S ′ is so, where S ′ does not contain case-defined functions.
Proof. Thanks to Lemma 7, in the rest of this proof we assume w.l.o.g. that an RDFS + -SAS S = (O, x, ι(x), m j=1 {τ j (x, x ′ )}) does not contain case-defined functions. Moreover, we require the following claim, an immediate consequence of the definitions. ι(x 0 ) ∧ τ j0 (x 0 , x 1 ) ∧ . . . ∧ τ j k−1 (x k−1 , x k ) ∧ ν(x k ) that is satisfiable w.r.t. O, for some k ≥ 0. By the observation above, we get that S is unsafe iff there is a formula ϑ of the form (⋆) that is satisfiable w.r.t. T (O), for some k ≥ 0. Thanks to Theorem 2, T (O) admits a model completion T (O) * . Hence, since the formulas of the form (⋆) are existential Σ T (O) -formulas, and by using the property that every model of an FO theory T embeds into a model of its model completion T * , we conclude that S is unsafe iff, for some k ≥ 0, there is a formula ϑ of the form (⋆) that is satisfiable in a model of T (O) * . Thus, for establishing (un)safety of S, we can concentrate on satisfiability of formulas of the form (⋆) in models of T (O) * .
We now continue the proof by adopting arguments similar to the ones contained in the proof of [11,Theorem 4.2]. We want to show the correctness of Algorithm 1. First, we preliminarily give some useful remarks on the algorithm. Let us call B n (resp. φ n ), with n ≥ 0, the status of the variable B (resp. φ) after n executions in Line 4 (resp. Line 6) of Algorithm 1 (n = 0 corresponds to the status of the variables in Line 1). Notice that we have for all j and that is an invariant of the algorithm. We now show that if the algorithm returns an unsafe outcome, this outcome is correct, i.e., S is really unsafe. Since we are considering satisfiability of formulae of the form (⋆) in models of T (O) * , we can apply the quantifier elimination procedure of T (O) * : it can be easily seen that the satisfiability of the quantifierfree formula we get in this way is equivalent to the satisfiability of ι ∧ φ n : clearly, this is again a quantifier-free formula (because of line 6 of Algorithm 1). Since T (O)-satisfiability and T (O) * -satisfiability are equivalent (by definition of model completion) when dealing with existential (and in particular, quantifier-free) formulae, the T (O)-satisfiability of ι ∧ φ n is decidable thanks to Theorem 2. Hence, if Algorithm 1 terminates with an unsafe outcome, then there exists a formula ϑ of the form (⋆) that is T (O) * -satisfiable. This exactly means that S is unsafe, as wanted.
We now show that if the algorithm returns a safe outcome, this outcome is correct, i.e., S is really safe. Consider the satisfiability test in Line 2. This is again a satisfiability test for a quantifier-free Σ T (O) -formula, thus it is decidable. In case of a safe outcome, we have that T (O) |= φ n → B n ; we claim that, if we continued executing the loop of Algorithm 1, we would get that for all m ≥ n. We justify Claim (3) below. From T (O) |= φ n → B n , taking into consideration that T (O) * ⊇ T (O) and that Formula (1) holds, we get T (O) * |= φ n+1 → P re(τ, B n ). Since P re commutes with disjunctions (i.e., P re(τ, j φ j ) is logically equivalent to