In the context of verification of data-aware processes, a formal approach based on satisfiability 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 define 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 flourishing series of results, within business process management [28,9,20] and data management [30,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,31]. 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,31] 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 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 controlflow, e.g., based on state machines [26] or Petri nets interpreted with interleaving semantics [20,27].
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.
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 ϕ ::
, 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.
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 (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.
Example 1. To represent part of the domain knowledge on job hiring processes for university personnel, we define the RDFS + ontology O = (T , A), where T consists of the following concept inclusions: 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
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(Γ ). 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 satisfiable w.r.t. O (or O-satisfiable) if there exists a model I of O that satisfies ϕ 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 |= ϕ, if, for every model I of O and every assignment a in I, we have that I satisfies ϕ under a.
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.
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 (Sketch). To prove Point (i), we reduce to RDFS + (seen as a fragment of ALCHI, [29]) ontology satisfiability. For Point (ii), since there is no function symbol in Σ T (O) , it is sufficient to show that T (O) enjoys the amalgamation property: this is proved by explicitly constructing a T (O)-amalgam for every pair of models I 1 and I 2 of T (O) sharing a submodel I 0 (see [12] for details). 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.
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].
We first require the following preliminary notions. For an RDFS + ontology O, an O-partition is a finite set P = {κ 1 (x), . . . , κ n (x)} of Σ O -literals such that O |= ∀x n i=1 κ i (x) ∧ ∀x i =j ¬(κ i (x) ∧ κ j (x)). Given an ontology O, an Opartition P = {κ 1 (x), . . . , κ n (x)}, and Σ O -terms t(x) = (t 1 (x), . . . , 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;
, for 1 ≤ j ≤ m, is a transition formula, where γ j (x, y) is a conjunction of Σ O -literals called guard of τ j , and x i = F j i (x, y), where each F j i is a case-defined 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 quantifier-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 infinite) set of states, because of the presence of (possibly infinitely many) different 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
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 + -SAS S = (O, x, ι(x), 7 j=1 {τ j (x, x )}) so that: the ontology O is the RDFS + ontology given in Example 1; the artifact variables are x = (x applicant , x job , x eligible , x winner , x loser ); the initial state formula is
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 ).
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 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).
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 definitions. Claim 1. For every safety formula ν(x) for S and every k ≥ 0, a formula ϑ of the form ( ) is satisfiable w.r.t. O iff ϑ is satisfiable w.r.t. T (O).
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. Proof (Sketch). For every RDFS + ontology O, there are only finitely many quantifier-free Σ T (O) -formulas, up to T (O)-equivalence, that can be built out of a finite set of variables x. Thanks to the availability of the quantifier elimination procedure QE(T (O) * , ϕ), 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, [29]), required in Lines 2 and 3.
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.
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 2014-2020, and by the Free University of Bozen-Bolzano through the projects KGID, GeoVKG, STyLoLa, VERBA and MENS.