Object-Centric Behavioral Constraints: Integrating Data and Declarative Process Modelling Wil van der Aalst1 , Alessandro Artale2 , Marco Montali2 and Simone Tritini2 1 Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands. w.m.p.v.d.aalst@tue.nl 2 Free University of Bozen-Bolzano, Piazza Domenicani 3, I-39100, Bolzano, Italy. surname@inf.unibz.it 1 Introduction Despite the plethora of notations available to model business processes, process mod- elers struggle to capture real-life processes in meaningful descriptions. Notations range from formal languages like Petri nets, automata and process algebras to dedicated mod- eling languages like Business Process Model and Notation (BPMN), Event-driven Pro- cess Chains (EPC) and UML activity diagrams. However, all such mainstream mod- eling languages suffer from two main issues. First, it is difficult to model interactions between process instances, which are in fact typically considered in isolation. Con- cepts like lanes, pools, and message flows in conventional languages like BPMN aim to address this. However, within each (sub)process still a single instance is modeled in iso- lation. Second, it is difficult to model the data-perspective and control-flow perspective in a unified and integrated manner. Data objects can be modeled, but the more powerful constructs present in Entity Relationship (ER) models and UML class models cannot be expressed well in process models. For example, cardinality constraints in the data model must influence behavior, but this is not reflected at all in today’s process models. Numerous practical applications of process mining [2] clearly show that there is a mismatch between process models and the data in real enterprise systems from ven- dors such as SAP (S/4HANA), Microsoft (Dynamics 365), Oracle (E-Business Suite), and Salesforce (CRM). Even though a clear process instance notion is missing in such systems, mainstream business process modeling notations can only describe the life- cycle of one type of process instance at a time. To overcome such critical issue and provide a unified representation of process and data-related constraints, the Object- Centric Behavioral Constraint (OCBC) model has been recently devised [10]. OCBC combines ideas from declarative, constraint-based languages like Declare [12, 11], and from data/object modeling techniques (such as ER, UML, or ORM). Cardinality con- straints are used as a unifying mechanism to tackle data and behavioral dependencies, as well as their interplay. Unlike existing approaches for process modeling, instances are not considered in isolation and cardinality constraints in the data/object model are taken into account. The driving modelling assumption underlying our proposal is that a process and its composing actions are identified by a unique instance (a sort of process id). By typing the process id with (possibly) different actions at (possibly) different points in time we 4 Create Pick Wrap Deliver Order Item Item Items 5 7 1 1 0..1 1 1 creates fills 2 8 3 prepares refers to 6 1 1 1 1 Order Order Delivery 1 contains * Line 1..* results in 0..1 * * * is for Product 1 belongs to receives Customer 1 1 Fig. 1. A small Object-Centric Behavioral Constraint (OCBC) model. model the different actions taking place in a given process. The action flows in a process is constrained using LTL-like axioms. To capture objects manipulated by actions we use relations whose domain are the actions and the range the object classes. Constraints are added to express possible co-references between objects manipulated by different actions. The following example shows the main ingredients of our proposal. Example 1. Fig. 1 shows an OCBC model for a process composed by four activities (CreateOrder, PickItem, WrapItem and DeliverItems) and five object classes (Order, OrderLine, Delivery, Product and Customer). The top part describes the ordering of activities and the bottom part the structuring of objects relevant for the process. The lower part can be read as a standard UML class diagram (e.g., an Order contains zero or more OrderLines while each OrderLine corresponds to precisely one Order, each OrderLine refers to one Product, each Order refers to one Customer, etc.). The top part shows behavioral constraints between the activities of the process and the middle part relates activities and data. To introduce the main ideas underlying our proposal, we informally describe the constructs highlighted in Fig. 1. 1 There is a one-to-one correspondence between a CreateOrder activity and an Order, i.e., the execution of a CreateOrder activity creates to a unique Order. 2 Every exe- cution of the PickItem activity refers to a unique OrderLine and each OrderLine can be picked exactly once. 3 Every execution of the WrapItem activity refers to an OrderLine and each OrderLine can be wrapped at most once. 4 Each CreateOrder activity is followed by one or more PickItem activities related to the same order. 5 Each PickItem activity is preceded by precisely one CreateOrder activity. 6 The two co-reference constraints (dash dotted lines) impose that when we create an order instance it will contain an order line eventually associated to a PickItem activity and, viceversa, to each order line associated to a PickItem activity corresponds an order as created by the CreateOrder activity. 7 Each WrapItem activity is preceded by one or more PickItem activities. 8 Two co-reference constraints (dash dotted lines) im- pose that when a PickItem activity fills an order line instance it will be the same as the one prepared by a WrapItem activity and, viceversa, an OrderLine prepared by a WrapItem must coincide with that one filled by a PickItem activity. A possible model of the OCBC model of Fig 1 is the following (we abbreviate names of activities and classes with their initials): CO(p1 , t0 ), PI(p1 , t1 ), PI(p1 , t2 ), WI(p1 , t3 ), WI(p1 , t4 ), PI(p1 , t5 ), WI(p1 , t6 ), DI(p1 , t7 ), DI(p1 , t8 ), creates(p1 , o1 , t0 ), contains(o1 , ol1 , t1 ), fills(p1 , ol1 , t1 ), contains(o1 , ol2 , t2 ), fills(p1 , ol2 , t2 ), prepares(p1 , ol1 , t3 ), prepares(p1 , ol2 , t4 ), contains(o1 , ol3 , t5 ), fills(p1 , ol3 , t5 ), prepares(p1 , ol3 , t6 ), results in(ol1 , d1 , t7 ), results in(ol2 , d1 , t7 ), refers to(p11 , d1 , t7 ), results in(ol3 , d2 , t8 ), refers to(p11 , d2 , t8 ). Note that the DeliverItems activity can deliver one or more OrderLines and that the OrderLines contained in an Order can be scattered over multiple Deliveries. The process described in the previous example cannot be modeled using conven- tional process modeling languages, because (a) three different types of instances (of ac- tivities, classes and also relationships instances) are intertwined in a uniform framework so that no further coding or annotations are needed, and (b) cardinality constraints and relations in the object class model influence the allowed behavior of activities and vicev- ersa. In the above example, interesting implicit constraints emerge from the interplay of the temporal constraints between activities and the cardinality constraints on activity- class and class-class relationships. For example, the temporal ordering of the activities logically implies that each Order will eventually contain at least one OrderLine. In this paper, we focus on the formal semantics of the OCBC model, so as to unam- biguously define the meaning of OCBC constraints, and in particular how the contribu- tion of the data and that of the temporal constraints among activities are intertwined. To do so, we employ first-order logic over the flow of time, i.e., first-order logic equipped with a special sort that represents time points and the usual < rigid binary relation. We then encode the resulting logical theory using temporal description logics, consequently paving the way towards automated reasoning over OCBC models and the identification of the corresponding boundaries of decidability and tractability. 2 Temporal Description Logics (HN ) In this paper we use the temporal description logic TUS DL-Litebool [6] to capture in a uniform formalism both the activities and their attached data. It is known from temporal logic [9] that all the temporal operators used in Linear Temporal Logic (LTL) can be ex- (HN ) pressed via S ‘since’ and U ‘until’. TUS DL-Litebool is one of the most expressive and still decidable temporal description logics which uses these two temporal operators. The language contains concept names CN0 , CN1 , . . . , flexible role names P0 , P1 , . . . , and rigid role names G0 , G1 , . . . . Role names S, roles R, basic concepts B and (temporal) concepts C are given by the following grammar: S ::= Pi | Gi and R ::= S | S − B ::= ⊥ | CNi | ≥ q R C ::= B | ¬C | C1 u C2 | C1 U C2 | C1 S C2 where S − denotes the inverse of the role S and q is a positive integer. We use the standard abbreviations: C1 t C2 = ¬(¬C1 u ¬C2 ), > = ¬⊥, ∃R = (≥ 1 R), ≤ q R = (HN ) ¬(≥ q + 1 R). A TUS DL-Litebool TBox, T , is a finite set of concept inclusion axioms of the form C1 v C2 , and of role inclusion axioms of the form R1 v R2 . A temporal interpretation is a structure of the form I = ((Z, <), ∆I , {·I(n) | n ∈ Z}), where (Z, <) is the linear model of time, ∆I is a non-empty interpreta- tion domain and I(n) gives a standard DL interpretation for each time instant n ∈ Z: I(n) I(n) I(n) = ∆I , CN0 , . . . , P0 , . . . , GI0 , . . . , assigning to each concept name CNi  I(n) I(n) a subset CNi ⊆ ∆I , to each flexible role name Pi a binary relation Pi ⊆ I I I I I ∆ × ∆ , while the interpretations Gi ⊆ ∆ × ∆ of rigid role names are the same for all n ∈ Z. The role and concept constructs are interpreted as follows, where C I(n) (RI(n) ) denotes the extension of C (R) at time n ∈ Z: I(n) (Pi− )I(n) = {(y, x) ∈ ∆I × ∆I | (x, y) ∈ Pi }, ⊥I = ∅, (≥ q R)I(n) = x ∈ ∆I | ]{y ∈ ∆I | (x, y) ∈ RI(n) } ≥ q ,  I(n) I(n) (¬C)I(n) = ∆I \ C I(n) , (C1 u C2 )I(n) = C1 ∩ C2 , I(k) [ \ I(m)  (C1 U C2 )I(n) = C2 ∩ C1 , k>n nm>k where ]X denotes the cardinality of X. Thus, for example, x ∈ (C1 U C2 )I(n) iff there is a moment k > n such that x ∈ C2I(k) and x ∈ C1I(m) , for all moments m between n and k. Note that the operators S and U (as well as the 2 and 3 operators to be defined below) are ‘strict’ in the sense that their semantics does not include the current moment of time. The non-strict operators, which include the current moment, are obviously definable in terms of the strict ones. Concept and role inclusion axioms are interpreted in I globally: I(n) I(n) I |= C1 v C2 iff C1 ⊆ C2 for all n ∈ Z; I(n) I(n) I |= R1 v R2 iff R1 ⊆ R2 for all n ∈ Z. with the following restriction on the interaction between role inclusions and cardinali- ties: no role R can occur in T in both a role inclusion of the form R0 v R and a number restriction ≥ q R or ≥ q R− with q ≥ 2. We call I a model of a TBox T and write I |= T if I satisfies all inclusions in T . A TBox T is satisfiable if it has a model. A concept C (role R) is satisfiable with respect to T if there are a model I of T and n ∈ Z such that C I(n) 6= ∅ (respectively, RI(n) 6= ∅). It is readily seen that the concept and role satisfiability problems are equivalent to TBox satisfiability. We now recall how to capture the other LTL operators (used in this paper) via the U and S operators. The operators 3F and 3P (‘sometime in the future/past’) can be expressed as 3F C = >U C and 3P C = >S C; the operators 2F (‘always in the future’) and 2P (‘always in the past’) are defined as dual to 3F and 3P : 2F C = ¬3F ¬C and 2P C = ¬3P ¬C. The nclusion C v 2 ∗ C captures rigid concepts by using the ‘always’ operator 2 ∗ , that can be expressed as 2∗ C = 2F 2P C, while the dual operator ‘sometime’ is defined as usual: 3 ∗ C = ¬2 ∗ ¬C. Finally, the temporal operators F (‘next time’) and P (‘previous time’) can be defined as F C = ⊥ U C and P C = ⊥ S C. response unary-response non-response A B A B A X B precedence unary-precedence non-precedence A B A B A X B responded-existence non-coexistence A B A X B Fig. 2. Types of BCM constraints. (HN ) Reasoning in TUS DL-Litebool w.r.t. to a TBox is a decidable problem which has been proven to be PSpace-complete in [6], i.e., the complexity of reasoning in LTL. 3 The OCBC Model In this section we present the main results of this paper, a formalization of what we call the OCBC model, i.e., a model where Object Classes and Behavioral Constraints are both present. In particular, the OCBC model simultaneously accounts for: (i) control- flow constraints, captured as declarative temporal dependencies between activities, tak- ing inspiration from the Declare language [1]; (ii) data dependencies, captured using standard data models that account for classes, relationships, and cardinality constraints; (iii) mutual relationships between activities and classes, so as to link the execution steps in the process with the data objects they manipulate; (iv) coreference constraints between instances of the data model associated to activities via the above mentioned relationships linking activities to data elements. We proceed as follows: we first show how behavioral constraints between activities (the so called Behavioral Constraints Model, BCM) can be formalized in Linear Tempo- ral Logic (LTL). As for the data model, we rely on well-established foundational results showing how standard data models can be suitably formalized in FOL and, in turn, en- coded into suitable DLs for reasoning [7, 3, 8]. We finally enrich the formalization by accounting for activity-class relationships, and coreference constraints. 3.1 The Behavioral Constraints Model BCM The BCM captures a set of declarative temporal constraints between (pairs of) activities, taking inspiration from the relation and negation Declare patterns [1]. Fig. 2 graphically renders the repertoire of behavioral constraints considered in this paper (also briefly sketching their relationship with Declare), while their textual representation is defined next. Definition 1 (BCM). A BCM is a triple: (UA , UBC , ΣBC ), where: – UA is the universe of the activities, denoted with capital letters A1 , A2 , . . .; Response(A, B) A v 3F B If A executes then B must be executed afterwards. Unary-Response(A, B) A v ¬B U (B u 2F ¬B) If A executes then B must be executed exactly once afterwards. Precedence(A, B) A v 3P B If A executes then B must have been executed before. Unary-Precedence(A, B) A v ¬B S (B u 2P ¬B) If A executes then B must have been executed exactly once before. Responded-Existence(A, B) Av3 ∗B If A executes then B must be executed either before or afterwards. Non-Response(A, B) A v 2F ¬B If A executes then B will never be executed afterwards. Non-Precedence(A, B) A v 2P ¬B If A executes then B was never executed before. Non-Coexistence(A, B) Av2 ∗ ¬B A and B cannot be both executed. Fig. 3. Semantics of control-flow constraints, where A and B are activities – UBC is the universe of the behavioral constraints that can be expressed between activities, UBC = {responded-existence, response, unary-response, precedence, unary-precedence, non-response, non-precedence, non-coexistence}, as shown in Fig. 2, where each bc ∈ UBC is a binary relation over activities, i.e., bc ⊆ UA ×UA ; – ΣBC is the set of control-flow constraints of the form bc(A1 , A2 ), where bc ∈ UBC and A1 , A2 ∈ UA . + When defining later on the OCBC model we will consider the set UBC of positive behav- ioral constraints, containing response, unary-response, precedence, unary-precedence, and responded-existence. The formal semantics of control-flow constraints is captured (HN ) via TUS DL-Litebool concept inclusion axioms (LTL-like formulas since roles are ab- sent), as shown in Fig. 3 together with their intuitive meaning. Example 2. Fig. 4 shows an example of a BCM describing the process flow of buying a ticket and its correlated activities. The arrow between SelectFlight and Payment rep- resents an unary-precedence constraint, thus when Payment is executed there must be a single execution of SelectFlight in the past. In case we Cancel Ticket then sometime in the past we should have done the Payment. We provide also examples of negative be- havioral constraints, e.g., when a Refund is executed then Check-In is never executed, i.e., if we cancel and then refund the ticket we can not do the check-in anymore. The corresponding TU S DL-LiteN bool axioms capturing the BCM of this example are: Payment v ¬SelectFlight S (SelectFlight u 2P ¬SelectFlight), Payment v ¬PrintTicket U (PrintTicket u 2F ¬PrintTicket), CancelTicket v 3P Payment, CancelTicket v 3F Refund, Refund v 2 ∗ ¬Check-In. Select Flight Payment Print Ticket Cancel Refund X Check-In Ticket Fig. 4. BCM example capturing the fragment of a ticket purchase process 3.2 The Class Model - ClaM We assume that data used by the activities conform to the ClaM data model. In this paper we consider a data model with basic constructs. For simplicity, we define here ClaM as a simplified version of UML, with object classes that can be organized along ISA hierarchies, binary relationships between object classes and cardinalities expressing participation constraints of object classes in relationships. More formally we have the following: Definition 2 (ClaM Syntax). A conceptual schema Σ in the Class Model, ClaM, is a tuple Σ = (UC , UR , τ, #src , #tar , ISA), where: – UC is the universe of object classes. We denote object classes as O1 , O2 , . . .; – UR is the universe of binary relationships among object classes. We denote rela- tionships as R1 , R2 , . . .; – τ : UR → UC × UC is a total function associating a signature to each binary relationship. If τ (R) = (O1 , O2 ) then O1 is the range and O2 the domain of the relationship; – #dom : UR × UC 6→ N × (N ∪ {∞}) is a partial function defining cardinality constraints of the domain of a relationship. The value #dom (R, O) is defined only if τ (R) = (O, O1 ); – #ran : UR × UC 6→ N × (N ∪ {∞}) is a partial function defining cardinality constraints of the range of a relationship. The value #ran (R, O) is defined only if τ (R) = (O1 , O); – ISA ⊆ UC × UC is a binary relation defining the super-class and sub-class hierar- chy on object classes. If ISA(C1 , C2 ) then C1 is said to be a sub-class of C2 while C2 is said to be a super-class of C1 . As for the formal set-theoretic semantics of ClaM and its translation to descrip- tion logics we refer to [7, 3]. In particular, cardinality constraints are interpeted as the number of times a given instance of the involved object class participates in the given relationships, while ISA is interpreted as sub-setting. To better clarify the elements of ClaM we show the following example. Example 3. We consider the example shown in Fig. 5, modelling a process flow (up- per part) and its associated data modeled via a ClaM diagram. Concerning the ClaM Deliver Cancel Luggage Flight 1 X Referred Buy Security Start Check-In Trip Controls flight 1 1 1 cref Create cref Generate Related 1 1..* 1 1..* 1..* 1..* Boarding 1..* 1 Ticket Flight IsAssociatedTo 1..* Card 1..* AssignedTo 1..* 1 1 1..* Buy Has Linked Traveller Luggage 1 Own 1..* Fig. 5. The OCBCM example of an airplane trip scenario. diagram we have that: UC = {Ticket, Traveller, Boarding-Card, Luggage, Flight}; UR = {IsAssociatedTo, Buy, Has, Own, Linked, AssignedTo}; τ (Own) = (Traveller,Luggage), . . . #dom (Own,Traveller) = (1, ∞); #ran (Own,Luggage) = (1, 1); . . . Note that cardinalities are depicted in the diagram in UML style. 3.3 The Object Centric Behavioral Constraint Model - OCBC The Object Centric Behavioral Constraint Model (OCBC) combines the behavioral con- straints model BCM capturing the process flow (as presented in Section 3.1) with the object classes represented by the ClaM data model (as presented in Section 3.2). The original proposal in the OCBC model is the way activities and data are related to each other and the formal underpinning of the model. We now present in details the syntax of an OCBC model. Definition 3 (The OCBC syntax). An OCBC model is a tuple: (BCM, ClaM, URAC , τRAC , #src , #tar , Ucrel ) where: – BCM is a behavioral constraint model as in Definition 1; – ClaM is a conceptual schema as in Definition 2; – URAC is the universe of activity-object relationships being a set of binary relation- ships; – τRAC : URAC → UA × UC is a total function associating a signature to each activity-object relationship. If τRAC (R) = (A, O) then A ∈ UA is the source and O ∈ UC the target of the relationship; – #src : URAC × UA → 7 N × (N ∪ {∞}) is a partial function defining cardinality con- straints on activities, i.e., constraints on the participation of activities in activity- object relationships. The value #src (R, A) is defined only if τRAC (R) = (A, O); – #tar : URAC × UC → 7 N × (N ∪ {∞}) is a partial function defining cardinality constraints on object classes, i.e., constraints on the participation of object classes in activity-object relationships. The value #tar (R, O) is defined only if τRAC (R) = (A, O); – Ucoref is the universe of coreference constraints being a set of functions, i.e., Ucoref = {cr | cr : ΣBC × URAC × URAC → UC ∪ UR }. To better understand the expressive power of the OCBC modelling language we discuss the scenario of an airplane travel. Example 4. Fig. 5 shows how an OCBC diagram captures an airplane trip scenario. The activities that belong to the process flow and modeled as a BCM diagram are depicted in the upper part of the figure. Then, in the lower part of the figure, we have the ClaM data model that captures the data manipulated by the activities of the process flow. The set URAC of the activity-object relationships is the following set of binary relationships: URAC = {Create, Generate, Referred, Receive, Related}, connecting an activity with the objects manipulated as an effect of executing the activ- ity itself. For example, the activity BuyTrip creates an instance of the object class Ticket when it is executed. Cardinality constraints can also be added to activity-object relation- ships to specify participation constraints either on the activity side or on the object class side. For example, at any point in the time, an execution of Check-in creates exactly one BoardingCard while each BoardingCard corresponds to exactly one Check-in action. Thus, #src (Generate, Check-in) = #tar (Generate, BoardingCard) = (1, 1). On the other hand, when we execute BuyTrip we can buy one or more tickets while a Ticket is associated to a single BuyTrip action. The coreference constraints (the dashed-dotted lines denotes as cref in Fig. 5) specify constraints on how objects connected to different activities can be shared. For example, the BoardingCard generated by a Check-in is the same used to deliver the luggage. This particular coreference constraint is specified as: cref(Unary-Precedence(DeliverLuggage, Check-in), Referred,Generate) = BoardingCard, while the other coreference constraints in Fig. 5 is expressed as: cref(Response(ButTrip, Check-in), Create,Generate) = IsAssociatedTo. In the next section we will present the semantics of OCBC models and we better clarify the two kinds of coreference constraints that can be involved in an OCBC model. Deliver Buy Check-In Check-In Luggage Trip cref Generate Referred Create cref Generate Boarding Boarding Ticket Card IsAssociatedTo Card (a) (b) Fig. 6. The two kinds of coreference: (a) over an object class, (b) over a relationship. 4 The OCBC Formal Semantics This section presents the semantics for OCBC models. In this respect, our effort is to reconcile the process flow semantics with the data model semantics associating to both worlds an FOL formalization and the corresponding temporal DL axioms. To capture the temporal nature of the whole framework we use a two sorted FOL with a sort dedicated to the time dimension. Thus, in the following, the variable t will denote a time point to be interpreted as an integer number. FOL formulas map activities and object classes to binary predicates while activity-object relationships and relation- ships of the data model to ternary relations. More formally, A ∈ UA ∪ UC is mapped in FOL as A(x, t); R ∈ URAC ∪ UR is mapped in FOL as R(x, y, t). As for the semantics of a BCM model, we already gave its meaning in Fig. 3 via the temporal DL translation. Concerning the semantic of the ClaM data model, we inter- pret it along the temporal semantics presented in [4, 5] for temporal data models. In the same papers, a mapping from a (temporal) data model to a temporal DL TBox is pre- sented and used in this paper. It is now crucial to formalize the meaning of coreference constraints. We proceed by assigning an FOL translation and then the corresponding (HN ) temporal DL in the form of a TUS DL-Litebool TBox extended with temporalized roles, i.e., roles of the form 3P R, 3F R, 2P R, 2F R, P R, F R, with the obvious meaning. All together, we will show how an OCBC model can be captured via a TBox (HN ) in TUS DL-Litebool thus resulting in a uniform representation. According to Defini- tion 3, there are two kinds of coreference constraints: the ones that range over ob- ject classes and the ones ranging over relationships. We start with the coreference over object classes as illustrated, e.g., in Fig. 6(a). Definition 4 (Semantics of coreference constraints over object classes). Let cr ∈ + Ucoref , bc ∈ UBC , R1 , R2 ∈ URAC , A1 , A2 ∈ UA and O ∈ UC s.t. bc(A1 , A2 ) ∈ ΣBC , τ (R1 ) = (A1 , O), τ (R2 ) = (A2 , O) and cr(bc(A1 , A2 ), R1 , R2 ) = O. Then, (HN ) the following FOL formula (in brackets the corresponding TUS DL-Litebool axioms) captures domain and range restrictions: ∀x, y, t.R1 (x, y, t) → A1 (x, t) ∧ O(y, t) (∃R1 v A1 , ∃R1− v O), (1) ∀x, y, t.R2 (x, y, t) → A2 (x, t) ∧ O(y, t) (∃R2 v A2 , ∃R2− v O), (2) while the semantics of the coreference is the following (in case bc is the constraint Response(A1 , A2 )): ∀x, y, t.R1 (x, y, t) → ∃t0 > t.R2 (x, y, t0 ) (R1 v 3F R2 ). (3) Similar formulas hold for other forms of positive behavioral constraints. We now consider the coreference over relationships as illustrated, e.g., in Fig. 6(b). In this case we need to consider two object classes in the data model that are related together with a relationship on which the coreference holds. In the DL translation, we need to use a role chain constructor with the following meaning: (R1 ◦ R2 )I(n) = I(n) I(n) {(x, y) ∈ ∆I × ∆I | ∃z.(x, z) ∈ R1 ∧ (z, y) ∈ R2 }. Definition 5 (Semantics of coreference constraints over relationships). Let cr ∈ + Ucoref , bc ∈ UBC , R1 , R2 ∈ URAC , A1 , A2 ∈ UA , O1 , O2 ∈ UC and R ∈ UR a relationships between O1 and O2 s.t. bc(A1 , A2 ) ∈ ΣBC , τ (R1 ) = (A1 , O1 ), τ (R2 ) = (A2 , O2 ) and cr(bc(A1 , A2 ), R1 , R2 ) = R. Then, the semantics of domain and range restrictions is as in Def. 4, while the semantics of the coreference when bc is a future constraint is the following (in case bc is the constraint Response(A1 , A2 )): ∀x, y, t. R1 (x, y, t) → ∃z, t0 . t0 > t ∧ R2 (x, z, t0 ) ∧ R(y, z, t0 ) (R1 v 3F (R2 ◦ R− )), (4) and when bc is a past constraint then (in case bc is the constraint Precedence(A1 , A2 )): ∀x, y, t. ∃z. R1 (x, z, t) ∧ R(z, y, t) → ∃t0 . t0 < t ∧ R2 (x, y, t0 ) (R1 ◦ R v 3P R2 ). (5) Similar formulas hold for other forms of behavioral constraints. 5 Considerations on Reasoning over OCBC Models The main motivation to provide a mapping to a DL TBox is the possibility offered by DLs to reason over TBoxes. As we observed, the temporal description logic used in (HN ) (HN ) this paper, TUS DL-Litebool , is decidable and PSpace-complete. TUS DL-Litebool is able to capture BCM diagrams thanks to its temporal capabilities. At the level of data (HN ) models, TUS DL-Litebool captures the main constructs of UML—with the exception of ISA between relationships and n-ary relationships—adding the possibility to express temporal constraints over both object classes and relationships (see [3, 5] for details). On the other hand, to fully capture OCBC models we need to go beyond the expres- (HN ) sivity of TUS DL-Litebool . Indeed, due to coreference constraints we need the expres- sivity of temporalised roles (see axiom (3)) or role chains (see axioms (4)-(5)). Both constructors can ruin the decidability of the resulting language. So, while reasoning over OCBC models without corefence constraints is a PSpace-complete problem the addition of coreferences makes reasoning an undecidable problem. One possibility to regain decidability, admitting just corefences over object classes, is to avoid at-most cardinality constraints on activity-object constraints (the undecid- ability proof in [6] relies on both temporalised roles and on the possibility to represent functional roles). The case with coreference constraints over relationships is more in- volved and requires further investigations. Indeed, it is well known that role inclusion axioms with role chains on the right-hand side (i.e., axioms of the form R v R1 ◦ R2 ) make the logic undecidable. It is to be understood whether the special form of role chains in OCBC models can still encode an undecidable problem. References 1. van der Aalst, W.M.P., Pesic, M.: Decserflow: Towards a truly declarative service flow lan- guage. In: The Role of Business Processes in Service Oriented Architectures (2006) 2. van der Aalst, W.M.P.: Process Mining: Data Science in Action. Springer (2016) 3. Artale, A., Calvanese, D., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Reasoning over extended ER models. In: Proc. of the 26th Int. Conf. on Conceptual Modeling (ER’07). LNCS, vol. 4801, pp. 277–292. Springer (2007) 4. Artale, A., Parent, C., Spaccapietra, S.: Evolving objects in temporal information systems. Annals of Mathematics and Artificial Intelligence 50(1–2), 5–38 (2007) 5. Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Complexity of reasoning over temporal data models. In: Proc. of the 29th Int. Conf. on Conceptual Modeling (ER’10). LNCS, vol. 4801, pp. 277–292. Springer (2010) 6. Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: A cookbook for temporal con- ceptual data modelling with description logics. ACM Transaction on Computational Logic (TOCL) 15(3) (2014) 7. Berardi, D., Calvanese, D., De Giacomo, G.: Reasoning on UML class diagrams. Artificial Intelligence 168(1–2), 70–118 (2005) 8. Franconi, E., Mosca, A., Solomakhin, D.: ORM2: formalisation and encoding in OWL2. In: Int. Workshop on Fact-Oriented Modeling (ORM’12). pp. 368–378 (2012) 9. Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press (1994) 10. Li, G., Montali, M., van der Aalst, W.M.P.: Object-centric behavioral constraints. Corr tech- nical report, arXiv.org e-Print archive (2017) 11. Montali, M., Pesic, M., van der Aalst, W.M.P., Chesani, F., Mello, P., Storari, S.: Declarative specification and verification of service choreographiess. ACM Transactions on the Web (TWEB) 4(1) (2010) 12. Pesic, M., Schonenberg, H., van der Aalst, W.M.: DECLARE: Full support for loosely- structured processes. In: Proc. of the Eleventh IEEE Int. Enterprise Distributed Object Com- puting Conference (EDOC’07). pp. 287–298. IEEE Computer Society (2007)