Despite the plethora of notations available to model business processes, process modelers struggle to capture real-life processes in meaningful descriptions. Notations range from formal languages like Petri nets, automata and process algebras to dedicated modeling languages like Business Process Model and Notation (BPMN), Event-driven Process Chains (EPC) and UML activity diagrams. However, all such mainstream modeling languages suffer from two main issues. First, it is difficult to model interactions between process instances, which are in fact typically considered in isolation. Concepts 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 isolation. 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 [
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 Deliver Items 1 refers to
1 Delivery
* receives Pick Item 1
7 fills 2 8
Wrap Item
0..1 3 prepares *
Line * is for 1 Customer 1
1 contains 1..* results in 0..1 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 execution 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) impose 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 conventional process modeling languages, because (a) three different types of instances (of activities, 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 viceversa. In the above example, interesting implicit constraints emerge from the interplay of the temporal constraints between activities and the cardinality constraints on activityclass 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 unambiguously define the meaning of OCBC constraints, and in particular how the contribution 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
In this paper we use the temporal description logic TUS DL-Lite(bHooNl ) [
S ::= Pi j Gi B ::= ? j CNi j and
R ::=
S j S q R
C ::= B j :C j C1 u C2 j C1 U C2 j 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); > = :?; 9R = ( 1 R); q R = :( q + 1 R): A TUS DL-Lite(bHooNl ) 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 ; f I(n) j n 2 Zg), where (Z; <) is the linear model of time, I is a non-empty interpretation domain and I(n) gives a standard DL interpretation for each time instant n 2 Z: I(n) = I ; CN0I(n); : : : ; P0I(n); : : : ; G0I ; : : : ; assigning to each concept name CNi a subset CNiI(n) I , to each flexible role name Pi a binary relation PiI(n)
I I , while the interpretations GiI I I of rigid role names are the same for all n 2 Z. The role and concept constructs are interpreted as follows, where CI(n) (RI(n)) denotes the extension of C (R) at time n 2 Z: (Pi )I(n) = f(y; x) 2 x 2
I I j (x; y) 2 PiI(n)g;
I j ]fy 2 I j (x; y) 2 RI(n)g q ; I n CI(n); (C1 u C2)I(n) = C1I(n) \ C2I(n); ?I = ;; ( q R)I(n) =
(:C)I(n) = (C1 U C2)I(n) = (C1 S C2)I(n) = [ C2I(k) \ k>n [ C2I(k) \ k<n \ CI(m) ;
1 n<m<k \ CI(m)
1 n>m>k where ]X denotes the cardinality of X. Thus, for example, x 2 (C1 U C2)I(n) iff there is a moment k > n such that x 2 C2I(k) and x 2 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 j= C1 v C2 iff I j= R1 v R2 iff
CI(n)
1 RI(n) 1
CI(n)
2 RI(n) 2 for all n 2 Z; for all n 2 Z: with the following restriction on the interaction between role inclusions and cardinalities: 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 j= 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 2 Z such that CI(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: 3C = : 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.
A A A
B B B
A
A response unary-response
non-response precedence unary-precedence non-precedence responded-existence non-coexistence B B
A A A
X X X
B B
B
(HN ) w.r.t. to a TBox is a decidable problem which has
Reasoning in TUS DL-Litebool
been proven to be PSpace-complete in [
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)
controlflow constraints, captured as declarative temporal dependencies between activities,
taking inspiration from the Declare language [
We proceed as follows: we first show how behavioral constraints between activities
(the so called Behavioral Constraints Model, BCM) can be formalized in Linear
Temporal 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,
encoded into suitable DLs for reasoning [
The BCM captures a set of declarative temporal constraints between (pairs of) activities,
taking inspiration from the relation and negation Declare patterns [
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; : : :; – UBC is the universe of the behavioral constraints that can be expressed between activities, UBC = fresponded-existence, response, unary-response, precedence, unary-precedence, non-response, non-precedence, non-coexistenceg, as shown in Fig. 2, where each bc 2 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 2 UBC and A1; A2 2 UA.
When defining later on the OCBC model we will consider the set UB+C of positive behavioral constraints, containing response, unary-response, precedence, unary-precedence, and responded-existence. The formal semantics of control-flow constraints is captured via TUS DL-Lite(bHooNl ) concept inclusion axioms (LTL-like formulas since roles are absent), 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 represents 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 behavioral 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 TUS DL-LitebNool axioms capturing the BCM of this example are: CancelTicket v 3P Payment;
Payment v :SelectFlight S (SelectFlight u 2P :SelectFlight); Payment v :PrintTicket U (PrintTicket u 2F :PrintTicket);
CancelTicket v 3F Refund;
Refund v 2 :Check-In: Cancel Ticket
Refund
X 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 relationships 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 [ f1g) 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 [ f1g) 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 hierarchy 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
description logics we refer to [
Example 3. We consider the example shown in Fig. 5, modelling a process flow (upper part) and its associated data modeled via a ClaM diagram. Concerning the ClaM
1 Referred
Security Controls
X Start flight 1
Related 1 1..*
Flight #dom(Own,Traveller) = (1; 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) combines the behavioral constraints 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 relationships; – RAC : URAC ! UA UC is a total function associating a signature to each activity-object relationship. If RAC (R) = (A; O) then A 2 UA is the source and O 2 UC the target of the relationship; – #src : URAC UA !7 N (N [ f1g) is a partial function defining cardinality constraints on activities, i.e., constraints on the participation of activities in activityobject relationships. The value #src(R; A) is defined only if RAC (R) = (A; O); – #tar : URAC UC !7 N (N [ f1g) 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 = fcr j cr : BC URAC URAC ! UC [ URg.
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 = fCreate; Generate; Referred; Receive; Relatedg; connecting an activity with the objects manipulated as an effect of executing the activity 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 relationships 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.
cref Boarding
Card (a) Generate 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 relationships of the data model to ternary relations. More formally,
A 2 UA [ UC R 2 URAC [ UR is mapped in FOL as is mapped in FOL as
A(x; t); 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
interpret it along the temporal semantics presented in [
All together, we will show how an OCBC model can be captured via a TBox in TUS DL-Lite(bHooNl ) thus resulting in a uniform representation. According to Definition 3, there are two kinds of coreference constraints: the ones that range over object 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 2 Ucoref, bc 2 UB+C , R1; R2 2 URAC , A1; A2 2 UA and O 2 UC s.t. bc(A1; A2) 2 BC , (R1) = (A1; O), (R2) = (A2; O) and cr(bc(A1; A2); R1; R2) = O. Then, (HN ) axioms) the following FOL formula (in brackets the corresponding TUS DL-Litebool captures domain and range restrictions: 8x; y; t:R1(x; y; t) ! A1(x; t) ^ O(y; t) 8x; y; t:R2(x; y; t) ! A2(x; t) ^ O(y; t) (9R1 v A1; (9R2 v A2; 9R1 v O); 9R2 v O); (1) 8x; y; t:R1(x; y; t) ! 9t0 > 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) = f(x; y) 2 I I j 9z:(x; z) 2 R1I(n) ^ (z; y) 2 R2I(n)g.
Definition 5 (Semantics of coreference constraints over relationships). Let cr 2 Ucoref, bc 2 UB+C , R1; R2 2 URAC , A1; A2 2 UA, O1; O2 2 UC and R 2 UR a relationships between O1 and O2 s.t. bc(A1; A2) 2 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)): 8x; y; t. R1(x; y; t) ! 9z; 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)): 8x; y; t. 9z. R1(x; z; t) ^ R(z; y; t) ! 9t0. t0 < t ^ R2(x; y; t0) (R1 R v 3P R2): (5) Similar formulas hold for other forms of behavioral constraints. 5
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
this paper, TUS DL-Lite(bHooNl ), is decidable and PSpace-complete. TUS DL-Lite(bHooNl ) is
able to capture BCM diagrams thanks to its temporal capabilities. At the level of data
models, TUS DL-Lite(bHooNl ) 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 [
On the other hand, to fully capture OCBC models we need to go beyond the expressivity of TUS DL-Lite(bHooNl ). Indeed, due to coreference constraints we need the expressivity 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
undecidability proof in [