Property Preservation in Adaptive Case Management

Abstract

Adaptive Case Management (ACM) has emerged as a key BPM technology for supporting unstructured business process, and has been used to support flexible services orchestration. A key problem in ACM is that case schemas need to be changed to best fit the case at hand. Such changes are ad-hoc, and may result in schemas that do not reflect the intended logic or properties. This paper presents a formal approach for reasoning about which properties of a case schema are preserved after a modification, and describes change operations that are guaranteed to preserve certain properties. The Case Management model used here is a variant of the Guard-Stage-Milestone model for declarative business artifacts. Applicability is illustrated using a real-life example.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Case management has been introduced to support knowledge intensive business processes, which are organized around data artifacts [8, 22, 25]. Case management often needs to support flexible business processes that are performed by knowledge workers. So case management schemas must be easy to change. Adaptive Case Management (ACM) has been proposed as umbrella term for flexible case management [20]. Case Management has been applied in many knowledge-worker driven application areas, including fraud detection, healthcare, education, and social work, and has also been used as a basis to support flexible services orchestration to enable collaboration between enterprises (e.g., [15, 17]).

Designing case management models is hard. The presence of business rules may make it difficult to assess and predict the behavior specified in a case management model or schema. However, changing case management schemas is even harder. Unwanted behavior such as logical errors can be easily introduced by changing a case management model. More generally, a change could have undesirable side effects. Therefore, certain user-defined properties should be preserved in the changed schema.

This paper studies conditions under which case management schemas can be changed while preserving specified properties. We use the Guard-Stage-Milestone (GSM) model; GSM schemas declaratively specify life-cycles of business artifacts. The meta-model underlying the OMG standard Case Management Model and Notation (CMMN) [3] is based on GSM. In this paper we use a restricted variant of the GSM model, called Fully Acyclic GSM, to enable a focus on the key ideas and the development of informative and useful results. We leave for future research the generalization of the approach to richer variants of GSM.

The paper makes three fundamental contributions. First, we develop a precise definition for testing the preservation of properties. This is based on the notion of conditional emulatability, which allows to specify a condition under which executions of one GSM schema can be imitated by executions of a second GSM schema. Second, we develop a general-purpose “Lifting Lemma”. Speaking intuitively, this provides a mechanism for isolating changes to a “local area” in a GSM schema. And third, we use the Lifting Lemma to show how key change operations can be defined so as to guarantee the preservation of certain properties. Importantly, the theoretical work is motivated by examples arising in a real-world application.

The remainder of this paper is structured as follows. Section 2 introduces the problem of changing GSM schemas based on a real-world example, and illustrates change operations that preserve specified properties. Section 3 formally introduces the GSM model used in this paper. Section 4 develops the Lifting Lemma, and Sect. 5 illustrates applications of the Lifting Lemma by defining general-purpose change operations that preserve selected properties. Section 6 describes related work, and Sect. 7 offers brief conclusions.

Due to space limitations, the presentation here is terse. To improve readability, several of the definitions and some of the results are presented in an informal style. A technical report [10] contains more details on the results.

2 Motivation

To introduce the problem of variability, we consider an example based on a real-world process from an international technology company, which has offices in different geographic regions of the world. In the process, business criteria for partner contracts are assessed. Each region has its own flavor of the process.

Example 2.1

The base process, called here ${\textsf {BCA}}^{base}$, is used for the main region and has the following activities (see Fig. 1). First, data is gathered needed to perform the assessment. Next, two activities are performed in parallel as a pre-check. The credit is checked to ensure that the credit limit of the partner is still valid. In parallel, the past performance of the partner is evaluated and checked. If both checks are successful, the pre-check succeeds and a detailed check is performed, which may either succeed or fail. If the pre-check has succeeded within three weeks, a bonus is paid to the team managing the deal.

Fig. 1.

Main business criteria assessment process (${\textsf {BCA}}^{base}$)

Table 1. Stages and guards for ${\textsf {BCA}}^{base}$ in Fig. 1

Figure 1 shows the lifecycle part of the GSM schema for this process. The lifecycle contains stages (rounded rectangles) which represent the business activities (in this paper, these are essentially (atomic) tasks that are not explicilty modeled within the GSM schema). Guards (diamonds) specify under which condition work in a stage is launched. Milestones (circles) represent business objectives that are achieved by stages to which they are attached or by important events. Guards and milestones have sentries (business rules) that specify when they are executed; these are shown in Tables 1 and 2. Sentries implicitly specify dependencies between stages and milestones: for instance, the sentry of the guard of stage Credit Check states that the stage is opened if milestone IDGS has been achieved, so the guard of Credit Check depends on IDGS. The dependencies are graphically depicted using dashed arrows in Fig. 1. (Our diagramatic convention does not explictly indicate how multiple milestones are combined in a sentry, e.g., the sentry for PCS; please refer to the tables.) Rectangles represent data attributes. A dashed line from a stage to a data attribute indicates that the stage computes a value for the data attribute. To compare different GSM schemas, we make use of output attributes, depicted in bold italics, which can be milestones or data attributes. Some attributes are not shown (spez., fast_turnaround computed by Fast Turnaround Business Eligibility and BP_good computed by Business Performance Evaluation Check).

The behavior of GSM schemas is driven by event occurrences, which are typically the result of completion of a stage execution. In response to an event occurrence, a B(usiness)-step is taken, in which as many sentries as possible are applied. For instance, suppose that in some “snapshot”, i.e., the state of an artifact instance at some time during its execution, the milestone BPECS is true and stages Credit Check and Fast Turnaround Bonus Eligibility are the only open stages. If stage completion event C:Credit Check now occurs with value 9 for rating, then milestone CCS gets achieved. The milestone PCS also gets achieved, and also stage Detailed Check is opened (and thus, the external activity associated with that stage is started). At this point no further sentries can be applied, the B-step is finished, and the new snapshot has been computed. (See also Example 3.5 below.)    $\square$

Table 2. Milestones for ${\textsf {BCA}}^{base}$ in Fig. 1

Fig. 2.

Process ${\textsf {BCA}}^{del}$ resulting after applying change of Example 2.3

We next present three variations on this example.

Example 2.2

In another region, the business performance of a partner is evaluated and checked only if the partner has more than 300 employees. The GSM schema of Fig. 1 is changed as follows (the other sentries are not changed):

• The guard of stage Business Performance Evaluation Check becomes $\textsf {IDGS} \wedge \textsf {employee\_count} \ge 300$.

• Milestone PCS can be achieved via extra sentry $\textsf {CCS} \wedge \textsf {employee\_count} < 300$.

Now the question arises how the change affects cases. We would like to assert that for partners with 300 or more employees, the new GSM schema emulates the behavior of the old GSM schema, and the old GSM schema emulates that of the new, so for the same cases, the same output results in both schemas. (‘Emulates’ is defined precisely in Definition 4.4 below.) For partners with less than 300 employees, this assertion does not hold. In particular, it may be that a company with say 290 employees and a poor performance is accepted under the new schema but rejected under the old schema. Example 5.2 will illustrate how the formalism and results of this paper can be applied to prove these properties.    $\square$

Example 2.3

Consider again the base process ${\textsf {BCA}}^{base}$ of Example 2.1. In yet another region, the credit of the partner is not checked. Schema ${\textsf {BCA}}^{base}$ is changed by deleting stage Credit check and milestones CCS and CCU, as visualized in ${\textsf {BCA}}^{del}$ in Fig. 2. The sentries of milestones PCS and PCU need to change as follows (the other sentries are not changed):

• The sentry of milestone PCS becomes BPECS.

• The sentry of milestone PCU becomes BPECU.

To characterize the change, we would like to assert that for cases under the old schema for which the credit check was successful, the new schema emulates the old schema. For cases of partners for which the credit check was unsuccessful in Fig. 1 there is a difference: for those cases the detailed check can be performed as in Fig. 2. This example will be revisited in Examples 4.5 and 4.11.    $\square$

Fig. 3.

Process ${\textsf {BCA}}^{ins}$ after applying change of Example 2.4

Example 2.4

Consider again the base process ${\textsf {BCA}}^{base}$. In a fourth region, the market addressed by the partner is assessed. Stage Addressable Market Check is inserted with milestones AMCS (Addressable Market Check Successful) and AMCU (Addressable Market Check Unsuccessful); see ${\textsf {BCA}}^{ins}$ in Fig. 3. The sentries need to change as follows (the other sentries are not changed):

• The guard of stage Addressable Market Check becomes $\textsf {IGDS} \wedge \textsf {annual\_revenue} \ge \$500K$;

• The sentry of milestone PCS is replaced with two sentries: $\textsf {CCS} \wedge \textsf {BPECS} \wedge \textsf {AMCS}$ and $\textsf {CCS} \wedge \textsf {BPECS} \wedge \textsf {annual\_revenue} < \$500K$.

• The sentry of milestone PCU becomes $\textsf {CCU} \vee \textsf {BPECU} \vee \textsf {AMCU}$.

The change assertion is that for cases in which the annual revenue is lower than $\$500K$, the old schema emulates the new schema and vice versa. Also for cases in which the annual revenue is higher or equal to $\$500K$ and the milestone AMCS gets achieved, the old and the new schema emulate each other. This will be revisited in Example 5.9.    $\square$

3 The Formal GSM Model

This section presents formal definitions for the variant of GSM used in this paper. This includes a specific notion of “executions” of a GSM schema, that will be important in our reasoning about property preservation. It is assumed that the reader is familiar with the basic aspects of the formal definitions of GSM (e.g., as in [6, 9, 14]).

The development here imposes a family of restrictions on the GSM variants of, e.g., [9, 14], to enable the development of interesting theoretical properties concerning schema evolution.A comparison of the GSM used here with previous variants is presented in [10]. Importantly, in the GSM variant used here, the executions are monotonic, that is, an attribute value does not change once it is defined.Generalization and adaptation of these results to richer variants of GSM, and to the full GSM model, are left for future research.

These assumptions enable a streamlined approach for the formal definitions of GSM schema and operational semantics.

We assume three infinite disjoint sets of names, for data attributes, for milestones, and for stages. Each data attibute a has a type ${\textit{type}}(a)$ which is scalar (e.g., string, character, integer, float, etc.), or is a set of records of scalars. Milestones can be used as attributes with type Boolean. Both data attributes and milestones may take the unassigned (or null) value (denoted $\bot$).

We assume a condition language $\mathcal {C}$ that includes fixed predicates over scalars (e.g., ‘$\le$’ over integers or floats), and Boolean connectives. Quantification and testing set membership is supported for working with the set-valued attributes. The condition formulas may involve stage, milestone, and data attributes. All attributes start with undefined value ($\bot$). Milestones will take the value ${\textit{True}}$ if one of their sentries go true. Stages will take the value ${\textit{True}}$ at the time when they complete. (This is a variation on the traditional behavior of stage attributes.)

A sentry $\psi$ has one of the three forms: “$\varphi$”, “${\mathsf{C:}}S$”, or “${\mathsf{C:}}S \wedge \varphi$”, where $\varphi$ is a condition formula ranging over the attributes of $\varGamma$. Here “${\mathsf{C:}}S$” is called the completion event for stage S. Also, ${\mathsf{C:}}S$ (if present) is the completion event for $\psi$ and $\varphi$ (if present) is the formula for $\psi$.

Definition 3.1

A GSM schema is a 5-tuple $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ where:

• 1. ${\textit{Att}}_d$ is a finite set of data attributes.

• 2. ${\textit{Att}}_m$ is a finite set of milestone attributes.

• 3. ${\textit{Att}}_{\textit{S}}$ is a finite set of stage attributes.

• 4. ${m_\mathrm{\small start}}\in {\textit{Att}}_m$ is called the start milestone. It is used as a mechanism for launching an execution of $\varGamma$.

• 5. ${\textit{Att}}_{{\textit{out}}}\subseteq {\textit{Att}}_d \cup {\textit{Att}}_m$ is the set of output attributes for $\varGamma$. This set is also denoted as ${\textit{out}}(\varGamma )$.

• 6. The sentry assignment ${\textit{sen}}$ is a function from ${\textit{Att}}_{\textit{S}}\cup (att_m - \{{m_\mathrm{\small start}}\})$ to sets of sentries with formulas in the condition language $\mathcal{C}$ ranging over ${\textit{Att}}$, and such that if there is a completion event ${\mathsf{C:}}S$ then $S \in {\textit{Att}}_{\textit{S}}$.

• 7. The signature assignment ${\textit{sig}}$ is a function from ${\textit{Att}}_{\textit{S}}$ to pairs (I, O) of finite sets of attributes from ${\textit{Att}}_d$ If ${\textit{sig}}(S) = (I,O)$, then we denote I as ${\textit{sig}}_{{\textit{in}}}(S)$, called the input of S, and denote O as ${\textit{sig}}_{{\textit{out}}}(S)$, called the output of S.

Sentries define dependencies between stage and milestone attributes of $\varGamma$. For $a_1,a_2 \in {\textit{Att}}_{\textit{S}}\cup {\textit{Att}}_m$, a dependency $(a_1,a_2)$ signifies that there is a sentry of $a_2$ that references $a_1$. The dependency graph of $\varGamma$, denoted ${DG}(\varGamma )$, contains all these dependencies [10]. Schema $\varGamma$ is Fully Acyclic if ${DG}(\varGamma )$ is a directed acyclic graph. Then $\varGamma$ is called an FA-GSM schema. Each FA-GSM schema is a GSM schema in the sense of earlier work [6, 9], and the equivalence theorem for B-steps developed there also holds for FA-GSM schemas.

Definition 3.2

For a GSM schema $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}},$ ${\textit{sen}}, {\textit{sig}})$ a snapshot is a mapping $\sigma$ from ${\textit{Att}}$ into values of appropriate type (where some attributes may be assigned the null value $\bot$). For milestone and stage attributes, the only permitted values are $\bot$ and ${\textit{True}}$.

In the GSM model used here, milestone and stage attributes will never take the value ${\textit{False}}$. This is because such attributes will remain undefined until they become true.

Definition 3.3

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ be a GSM schema. Let $\mu$ be a sentry for miletone m, and let $\varphi$ be the formula of $\mu$. Given a snapshot $\sigma$ of $\varGamma$ (where some attributes may have undefined value), $\varphi$ is strictly satisfied by $\sigma$, denoted $\sigma \models ^{strict}\varphi$, if $\sigma$ is non-null for each attribute A occurring in $\varphi$, and if $\varphi$ is satisfied by $\sigma$.

Now let $\varphi$ be the formula of a sentry for a stage S. For snapshot $\sigma$ of $\varGamma$, $\varphi$ is strictly satisfied for S by $\sigma$, denoted $\sigma \models ^{strict}_S \varphi$, if (a) $\sigma$ is non-null for each attribute in ${\textit{sig}}_{{\textit{in}}}(S)$, (b) $\sigma$ is non-null for each attribute occurring in $\varphi$, and (c) $\varphi$ is satisfied by $\sigma$.

In particular, if $\sigma \models ^{strict}_S \varphi$, then each input attribute for S is defined, and so S can be launched. In this paper we focus on strict satisfaction, and refer to this simply as “satisfaction”.

The notion of B-step for a FA-GSM schema $\varGamma$ and snapshot $\sigma$ is defined as in [6, 9]. Further, it can be verified that the basic equivalence results from [6] apply to FA-GSM schemas.

Definition 3.4

Let $\varGamma$ be an FA-GSM schema. An execution of $\varGamma$ is a sequence

$$\begin{aligned} \xi \ = \ ({\sigma _{init}}, \sigma _0, \alpha _1, \beta _1, \sigma _1, \dots , \alpha _n, \beta _n, \sigma _n) \end{aligned}$$

where (a) the $\sigma$’s are snapshots; (b) ${\sigma _{init}}$ is special initial snapshot that is essentially all false except for ${m_\mathrm{\small start}}$ which is assumed to have just turned to ${\textit{True}}$; (c) each $\sigma _i$ is the result of a B-step based on the preceding $\sigma$ and (for $i > 0$) the incoming stage completion, denoted as $\beta _i$. Stages may be launched as part of a B-step; the set of these are represented by the $\alpha$’s. The family of executions of $\varGamma$ is denoted ${\textit{Exec}}(\varGamma )$.

An execution is terminal if it cannot be extended. The set of terminal executions is denoted ${\textit{TermExec}}(\varGamma )$.

Example 3.5

We illustrate the notion of execution by revisiting Example 2.1 and the B-step described there. Snapshots are denoted here by listing all milestones that are true, all stages that are open, and the value of each defined data attribute. In each execution of ${\textsf {BCA}}^{base}$, $\sigma _0$ = {Initial Data Gathering}. After that stage completes, we might arrive at $\sigma _1$ that additionally has milestone IDGS true, and each of Credit Check, Business Performance Evaluation Check, and Fast Turnaround Bonus Eligibility open. Also, $\alpha _2$ holds these three stage names. The next steps of the execution might be as follows.

The B-step of Example 2.1 occurs from $\beta _3$ to $\sigma _3$.    $\square$

4 Reasoning About GSM Executions

This section develops tools for reasoning about GSM executions, including comparing the executions supported by different FA-GSM schemas. The first subsection introduces the notion of stage i/o assignments, used to formally study the possible behaviors of stage executions. The second subsection defines conditional emulation, which provides the basis for formally comparing the behaviors of FA-GSM schemas. And the third subsection presents the Lifting Lemma.

4.1 Stage i/o Assignments

A primary goal of this paper is to study the preservation of properties when transforming an FA-GSM schema $\varGamma ^1$ into a related FA-GSM schema $\varGamma ^2$. To accomplish this we study properties of elements of ${\textit{Exec}}(\varGamma ^1)$ vis-a-vis elements of ${\textit{Exec}}(\varGamma ^2)$. Non-determinism in executions of an FA-GSM $\varGamma$ may lead to different outcomes for the same input, which complicates a fair comparison among executions of different schemas. There are two ways that non-determinism arises:

• Different Stage Outputs: Since many stages correspond to human activities, the outputs may vary due to a variety of factors that are not explicitly available in the snapshot that launched the stage containing that stage.

• Different Stage Completion Timing: Because sentries may include stage completion events, there may be “race” conditions under which a sentry does or does not fire. For example, consider sentry $\psi = {\mathsf{C:}}S \wedge \varphi$. Suppose that in a particular execution $\xi$ stage S completes before all variables in $\varphi$ have become defined. Then $\psi$ can never be triggered in $\xi$. In contrast, if S completes after all variables in $\varphi$ have become defined then $\psi$ might trigger in $\xi$.

The next definition allows us to focus on pairs of executions for which all shared stages have the same behavior.

Definition 4.1

Given FA-GSM schema $\varGamma$ a stage i/o assignment is a function $\tau$ with domain the stages of $\varGamma$, such that for each stage S, $\tau [S]$ is a function whose signature matches the signature of S in $\varGamma$.

An execution $\xi = {\sigma _{init}}, \sigma _0,\alpha _1,\beta _1,\dots ,\sigma _n$ of $\varGamma$ is compliant with $\tau$ if for each $i \in [1..n]$, the payload of the stage completion $\beta _i = {\mathsf{C:}}S(c_1,\dots ,c_p)$ corresponds to the application of $\tau [S]$ on the values from the snapshot that launched S.

Example 4.2

Let IDG denote stage Initial Data Gathering of ${\textsf {BCA}}^{base}$, and BPEC denote Business Performance Evaluation Check. In one stage i/o assignment $\tau _\mathsf{ABC}$ for the ABC company, we might have

Because the evaluations of business performance may be subjective, a different stage i/o assignment $\tau _\mathsf{ABC}'$ might arise, with $\tau _\mathsf{ABC}'[\mathsf{IDG}] = \tau _\mathsf{ABC}[\mathsf{IDG}]$ but $\tau _\mathsf{ABC}'[\mathsf{BPEC}](\mathsf{BP\_good}) = {\textit{False}}$.    $\square$

We use the stage i/o assignment to “explain” the output of stages in a particular execution. Intuitively, the following result states that the full range of nondeterminism in GSM executions can be controlled by holding the stage behaviors and the relative timing of stage completion fixed (proof omitted).

Lemma 4.3

If two executions of $\varGamma$ are compliant with the same stage i/o assignment, and if the order of stage completions is the same, then they are identical in all other ways as well.

4.2 Conditional Emulation

In the general case, we shall be looking at a pair $\varGamma ^1,\varGamma ^2$ of FA-GSM schemas and attempting to compare elements of ${\textit{TermExec}}(\varGamma ^1)$ with elements of ${\textit{TermExec}}(\varGamma ^2)$. We typically focus on executions that satisfy a condition, e.g., in the case of Example 2.2, $\varOmega$ = “employee count $\ge 300$”. We then demonstrate that executions of one schema that satisfy the condition can be emulated by executions of the other, e.g., for each execution of ${\textsf {BCA}}^{mod}$ that satisfies $\varOmega$ there is a corresponding execution of ${\textsf {BCA}}^{base}$ that behaves identically on output attributes PCU, DCS, and recommendation (see Example 5.2 below).

In the sequel, if f is a function over domain D, and $C \subseteq D$, then $f | _C$ denotes the restriction of f to C.

Suppose now that $\varGamma ^i = ({\textit{Att}}^i = {\textit{Att}}_d^i \cup {\textit{Att}}_m^i \cup {\textit{Att}}_{\textit{S}}^i, {m_\mathrm{\small start}}^i, {\textit{Att}}_{{\textit{out}}}^i, {\textit{sen}}^i, {\textit{sig}}^i)$ for i in [1,2]. Suppose further that $\tau ^i$ is a stage i/o assignment for $\varGamma ^i$, i in [1, 2]. Then $\tau ^1$ and $\tau ^2$ are compatible if $\tau ^1 | _{{\textit{Att}}_{\textit{S}}^1 \cap {\textit{Att}}_{\textit{S}}^2} = \tau ^2 | _{{\textit{Att}}_{\textit{S}}^1 \cap {\textit{Att}}_{\textit{S}}^2}$.

Let $\varGamma ^1,\varGamma ^2$ be as above. As suggested above, we shall work with conditions $\varOmega$ over the union ${\textit{Att}}^1 \cup {\textit{Att}}^2$, in order to focus on executions of $\varGamma ^1$ or $\varGamma ^2$ of interest. For a snapshot $\sigma ^1$ over $\varGamma ^1$, $\sigma ^1$ satisfies $\varOmega$ with existential extension, denoted $\sigma ^1 \models ^{ex}\varOmega$, if there is some extension $\sigma$ of $\sigma ^1$ to include all attributes of $\varOmega$ not in ${\textit{Att}}^1$, such that $\sigma \models ^{strict}\varOmega$.

We now define the notion of “conditional emulatability”, which enables us to compare the behavior of pairs of schemas with regards to selected attributes.

Definition 4.4

Let $\varGamma ^i = ({\textit{Att}}^i = {\textit{Att}}_d^i \cup {\textit{Att}}_m^i \cup {\textit{Att}}_{\textit{S}}^i, {m_\mathrm{\small start}}^i, {\textit{Att}}_{{\textit{out}}}^i, {\textit{sen}}^i, {\textit{sig}}^i)$ be an FA-GSM schema for i in [1,2], and let $\mathcal{A}\subseteq {\textit{Att}}^1 \cap {\textit{Att}}^2$, and let $\varOmega$ be a condition over ${\textit{Att}}^1 \cup {\textit{Att}}^2$. Then $\varGamma ^1$ emulates $\varGamma ^2$ under $\varOmega$, denoted $\varGamma ^1{\rightharpoonup _{\varOmega ,\mathcal{A}}} \varGamma ^2$, if the following holds. If

• 1. $\tau ^2$ is a stage i/o assignment for $\varGamma ^2$;

• 2. $\xi ^2 \in {\textit{Exec}}(\varGamma ^2)$ is a (possibly non-terminal) $\tau ^2$-compliant execution with final snapshot $\sigma ^2$; and

• 3. $\sigma ^2 \models ^{ex}\varOmega$

then

• 1. there exists a stage i/o assignment $\tau ^1$ for $\varGamma ^1$ that is compatible with $\tau ^2$, and

• 2. there exists a $\tau ^1$-compliant execution $\xi ^1 \in {\textit{Exec}}(\varGamma ^1)$ with final snapshot $\sigma ^1$,

• 3. such that $\sigma ^1 | _\mathcal{A}= \sigma ^2 | _\mathcal{A}$.

We write $\varGamma ^1{\rightleftharpoons _{\varOmega ,\mathcal{A}}} \varGamma ^2$ if $\varGamma ^1{\rightharpoonup _{\varOmega ,\mathcal{A}}} \varGamma ^2$ and $\varGamma ^2{\rightharpoonup _{\varOmega ,\mathcal{A}}} \varGamma ^1$.

Example 4.5

Recall ${\textsf {BCA}}^{base}$ (Example 2.1) and ${\textsf {BCA}}^{del}$ (Example 2.3). Let $\mathcal{A}$ = PCS, PCU and $\varOmega$ = “Rating = 9”. We illustrate now how it can be shown that $\varGamma ^1{\rightleftharpoons _{\varOmega ,\mathcal{A}}} \varGamma ^2$. For the ${\rightharpoonup _{}}$ direction, fix stage i/o assignment $\tau ^2$ for $\varGamma ^2$. We focus here on executions $\xi ^2$ of $\varGamma ^2$ where IDGS is satisfied. In those cases, the only $\tau ^1$ that extends $\tau ^2$ and enables satisfaction of $\varOmega$ will have $\tau ^1$[Credit Check](Rating) = 9. For this $\tau ^1$, the stage Credit Check will execute and return Rating with value 9 and trigger the milestone CCS. Thus, an execution $\xi ^1$ compliant with $\tau ^1$ can be constructed from $\xi ^2$ by inserting the launch and completion of Credit Rating sometime in between the satisfaction of IDGS and satisfaction of CCS. Emulation in the other direction is straightforward to show.    $\square$

4.3 The Lifting Lemma

The Lifting Lemma will enable us to infer emulatability in terms of output attributes, i.e., at a “global level”, based on emulatability in terms of selected milestone attributes, i.e., at a “local level”.

To state the lifting lemma we need to be able to talk about the areas where schemas $\varGamma ^1,\varGamma ^2$ differ.

Definition 4.6

Let $\varGamma ^1,\varGamma ^2$ be FA-GSM schemas, and let $\varDelta ^i$ be a subset of the stages and milestones of $\varGamma ^1$ for i in [1,2]. Then $\varDelta ^1,\varDelta ^2$ is a change pair for $\varGamma ^1,\varGamma ^2$ if the two schemas are identical except for the milestones and stages (and their sentries) in the delta’s.

Next, we introduce the notion of “fence” that allows us to create a separation between a change set and an output attribute.

Definition 4.7

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ be an FA-GSM schema, let $\varDelta \subset {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}$, and let $\mathcal{O}\subseteq {\textit{Att}}_{{\textit{out}}}$. A set $\mathcal{F}\subseteq {\textit{Att}}_m$ is a fence between $\varDelta$ and $\mathcal{O}$ if for each pair $\delta \in \varDelta , o \in \mathcal{O}$ and each path $\rho$ from $\delta$ to o in ${DG}(\varGamma )$ there is some $m \in \mathcal{M}$ on path $\rho$.

Speaking intuitively, if $\mathcal{F}$ is a fence between $\varDelta$ and $\mathcal{O}$, and if certain “race” conditions do not hold, then the values assigned to $\mathcal{O}$ will not be impacted by the behavior in the $\varDelta$ area. The next definition identifies the “race” conditions that need to be avoided (see Example 4.9 below).

Definition 4.8

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ be an FA-GSM schema, $\mathcal{F}\subseteq {\textit{Att}}_m$ a set of milestones in $\varGamma$, and $v \in {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}$. Then v is completion independent modulo $\mathcal{F}$ if for each stage $S \in {\textit{Att}}_{\textit{S}}$ and each path $\rho$ from S to v, if there is a node w on $\rho$ with a sentry of form “${\mathsf{C:}}S \dots$”, then there is a node $f \in \mathcal{F}$ that lies between w and v in $\rho$.

Example 4.9

In ${\textsf {BCA}}^{base}$, with the exception of bonus and TBPS, all output attributes are completion independent modulo $\{PCS\}$. In contrast, bonus and TBPS are not, because of the completion event C: Fast Turnaround Bonus Eligibility in the guard for stage Team Bonus Pay.    $\square$

We now have the Lifting Lemma, which states that under certain conditions, if $\varGamma ^1$ emulates $\varGamma ^2$ for the elements of a fence, then $\varGamma ^1$ also emulates $\varGamma ^2$ for output attributes that are downstream from that fence. The proof, omitted, is based on splicing of executions.

Lemma 4.10

(Lifting Lemma). Let $\varGamma ^i = ({\textit{Att}}^i = {\textit{Att}}_d^i \cup {\textit{Att}}_m^i \cup {\textit{Att}}_{\textit{S}}^i, {m_\mathrm{\small start}}^i$, ${\textit{Att}}_{{\textit{out}}}^i, {\textit{sen}}^i, {\textit{sig}}^i)$ be an FA-GSM schema for i in [1,2]. Suppose that:

• 1. $\varDelta ^1,\varDelta ^2$ is a change pair for $\varGamma ^1,\varGamma ^2$.

• 2. $\mathcal{O}\subseteq {\textit{out}}(\varGamma ^1) \cap {\textit{out}}(\varGamma ^2)$.

• 3. $\mathcal{F}$ is a fence between $\varDelta ^i$ and $\mathcal{O}$ in $\varGamma ^i$ for i in [1,2].

• 4. $\mathcal{O}$ is completion independent modulo $\mathcal{F}$ in $\varGamma ^i$, for i in [1,2].

• 5. $\varOmega$ is a condition over ${\textit{Att}}^1 \cup {\textit{Att}}^2$.

• 6. $\varGamma ^1{\rightharpoonup _{\varOmega ,\mathcal{F}}} \varGamma ^2$.

Then $\varGamma ^1{\rightharpoonup _{\varOmega ,\mathcal{O}}} \varGamma ^2$.

We next apply the Lifting Lemma to the example of deletion from Sect. 2.

Example 4.11

Recall Example 4.5, and the property ${\textsf {BCA}}^{base}{\rightleftharpoons _{\varOmega ,\mathcal{A}}} {\textsf {BCA}}^{del}$, where $\mathcal{F}= \{\textsf {PCS},\textsf {PCU}\}$ and $\varOmega$ = “rating = 9”. Let $\varDelta ^1$ = {Credit Check, CCS, CCU, PCS, PCU} and $\varDelta ^2$ = {PCS, PCU}. Then $\varDelta ^1, \varDelta ^2$ is a change pair for $\varGamma ^1,\varGamma ^2$. It is straightforward to verify that $\mathcal{F}$ is a fence between these change sets and the output attributes $\mathcal{O}$ = {IDGU, PCU, recommendation, DCS, DCU}. Thus, by the Lifting Lemma, $\varGamma ^1{\rightleftharpoons _{\varOmega ,\mathcal{O}}} \varGamma ^2$. Intuitively, this states that $\varGamma ^1,\varGamma ^2$ have identical behavior on $\mathcal{O}$, if the rating attribute is assumed to have value 9. There are no guarantees with regards to the attribute bonus), because of a possible race condition involving the completion of Fast Turnaround Bonus Eligibility, which occurs in the sentry for Team Bonus Pay.

However, note that bonus and TBPS have a completion dependency on Fast Turnaround Bonus Elibibility that is not blocked by $\mathcal{F}$. As a result, the Lifting Lemma does not apply to those attributes. Indeed, it is possible to construct an example execution $\xi ^1$ of $\varGamma ^1$ where Team Bonus Pay is not launched, but in the corresponding execution $\xi ^2$ of $\varGamma ^2$ this stage would launch.

Note that if the completion event C: Fast Turnaround Bonus Eligibility in the guard for Team Bonus Pay were dropped, then Term Bonus Pay, TBPS, and bonus would be completion independent modulo $\mathcal{F}$, and so the Lifting Lemma would apply to them.    $\square$

5 Property Preserving Schema Modifications

This section presents operators for modifying FA-GSM schemas that guarantee the preservation of various properties. The operators focus on sentry modification, and on deletions and insertions of stages and milestones. The proofs about property preservation rely on the Lifting Lemma. (The proofs are omitted here, but available in [10].) Examples from Sect. 2 are used to illustrate the results developed here.

We begin with a useful observation that is a very straightforward consequence of the Lifting Lemma. Before making the observation, we need the following: the notion of “shadow” of a change set Specifically, the shadow of $\varDelta$ is the set of milestones, stages, and data attributes that are “downstream” of nodes in $\varDelta$ in the graph $DG(\varGamma )$.

Let $\varDelta ^1,\varDelta ^2$ be a change pair for FA-GSM schemas $\varGamma ^1,\varGamma ^2$. It is easily shown that $\mathrm{ shadow}(\varDelta ^1,\varGamma ^1) = \mathrm{ shadow}(\varDelta ^2,\varGamma ^2)$.

Proposition 5.1

Let $\varGamma ^i = ({\textit{Att}}^i = {\textit{Att}}_d^i \cup {\textit{Att}}_m^i \cup {\textit{Att}}_{\textit{S}}^i, {m_\mathrm{\small start}}^i, {\textit{Att}}_{{\textit{out}}}^i, {\textit{sen}}^i, {\textit{sig}}^i)$ for i in [1,2], and let $\varDelta ^1,\varDelta ^2$ be a change pair for $\varGamma ^1,\varGamma ^2$. Let $\mathcal{A} = \mathrm{ shadow}(\varDelta ^1,\varGamma ^1) = \mathrm{ shadow}(\varDelta ^2,\varGamma ^2)$, and let $\mathcal{O}= ({\textit{Att}}_{{\textit{out}}}^1 \cup {\textit{Att}}_{{\textit{out}}}^2) - \mathcal{A}$. Then $\varGamma ^1{\rightleftharpoons _{True,\mathcal{O}}} \varGamma ^2$.

We next examine a simple form of sentry modification.

Example 5.2

Consider ${\textsf {BCA}}^{base}$ from Example 2.1 and ${\textsf {BCA}}^{mod}$ from Example 2.2. Recall that ${\textsf {BCA}}^{mod}$ is formed from ${\textsf {BCA}}^{base}$ by modifying the sentry on Business Performance Evaluation Check, to skip launching of that stage if the client has $<$ 300 employees, and adding a sentry for milestone PCS. Let $\varOmega$ = “employee_count $\ge 300$”. A case-by-case argument can be used to show that ${\textsf {BCA}}^{base}{\rightleftharpoons _{\varOmega ,\{\textsf {PCS}, \textsf {PCU}\}}} {\textsf {BCA}}^{mod}$. Now let

• $\mathcal{O}$ = {IDGU, PCU, recommendation, DCS, DCU}.

• $\varDelta ^1$ = {Business Performance Evaluation Check, BPECS, BPECU, PCS}.

• $\varDelta ^2$ = {PCS}.

Similar to Example 4.11, it is easily verified that $\mathcal{F}$ = {PCS, PCU} is a fence for $\varDelta ^i$ and $\mathcal{O}$, for i in [1,2]. Further, $\mathcal{O}$ is completion-independent modulo $\mathcal{F}$. The Lifting Lemma now implies that $\varGamma ^1{\rightleftharpoons _{\varOmega ,\mathcal{O}}} \varGamma ^2$.    $\square$

5.1 Deletion

This subsection develops constructions for deleting milestones and stages from FA-GSM schemas. Similar to the examples of Sect. 2, the focus is on enabling the deletions while maximizing emulatability.

We begin by describing the construction for deleting a single milestone. We shall use two notational conventions. The first is for substitutions in sentries: given a sentry $\psi$, an attribute z, and a formula $\varphi$, $\psi [z/\varphi ]$ denotes the result of replacing all occurrences of z in $\psi$ by $(\varphi )$. The second is a manipulation on sentries called completion-event removal: For a sentry of form $\psi = {\mathsf{C:}}S \wedge \varphi$, define ${\textit{cer}}(\psi )$ to be $S \wedge \varphi$. Notice that $\psi$ will be true for the single B-step where stage S completes, whereas ${\textit{cer}}(\psi )$ will be true for that B-step and all subsequent B-steps. If $\psi$ does not include a completion event, If $\psi$ is eventless, then ${\textit{cer}}(\psi ) = \psi$.

The following definition specifies implicitly an algorithm for deleting a milestone while preserving all output behaviors.

Definition 5.3

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ be an FA-GSM schema, m a milestone of $\varGamma$, and $M = \{\psi _1,\dots ,\psi _q\}$ the set of sentries of m in $\varGamma$. The deletion of m from $\varGamma$, denoted ${\textit{del}}(\varGamma ,m)$, is the FA-GSM schema constructed from $\varGamma$ in the following way. Suppose that v is a stage or milestone in $\varGamma$, that $\chi$ is a sentry for v, and that m occurs in $\chi$. Then replace $\chi$ in $\varGamma$ with a set of sentries

$$\begin{aligned} N = \{ \chi [m/{\textit{cer}}(\psi _p)] \mid p \in [1,q]\} \end{aligned}$$

Finally, delete m from the set of attributes of $\varGamma$.

Intuitively, in the construction of schema ${\textit{del}}(\varGamma ,m)$ occurrences of m in sentries are replaced by “macro-expansions” of m. It can be shown that in this construction, the set $\mathcal{F}$ of stages and milestones whose sentries are changed can serve as a fence, and that $\varGamma {\rightleftharpoons _{{\textit{True}},\mathcal{F}}} {\textit{del}}(\varGamma ,m)$.

Deleting a stage S from an FA-GSM schema $\varGamma$ is similar to deleting a milestone, in terms of performing “macro-expansions” in selected sentries. However, there are three complications. First, data attributes produced by S are assigned default values $\overrightarrow{c}$. Second, use of the default values must be delayed until S would have completed. And third, sentries that include S or ${\mathsf{C:}}S$ must be rewritten.

Definition 5.4

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ be an FA-GSM schema, S a stage of $\varGamma$, and $M = \{\psi _1,\dots ,\psi _q\}$ the set of sentries of m in $\varGamma$. Let $\overrightarrow{a} = {\textit{sig}}_{{\textit{out}}}(S)$ and let $\overrightarrow{c}$ be a vector of constants having types that match $\overrightarrow{a}$. The deletion of S from $\varGamma$ using $\overrightarrow{c}$ for $\overrightarrow{a}$, denoted ${\textit{del}}(\varGamma ,S,\overrightarrow{a}/\overrightarrow{c})$, is an FA-GSM schema constructed from $\varGamma$ in the following way. Suppose that v is a stage or milestone in $\varGamma$, that $\chi$ is a sentry for v, and that $\chi$ includes ${\mathsf{C:}}S$ and/or includes one or more attribute from $\overrightarrow{a}$. Then replace $\chi$ with a set of sentries

$$\begin{aligned} N = \{ \chi [{\mathsf{C:}}S/\psi _p, \overrightarrow{a}/\overrightarrow{c}] \wedge {\textit{cer}}(\psi _p) \mid p \in [1,q]\}. \end{aligned}$$

Finally, delete S from ${\textit{Att}}_{\textit{S}}$.

Example 5.5

To illustrate the above construction, consider a variation ${\textsf {BCA}}^{del}_{var}$ of ${\textsf {BCA}}^{del}$, in which only the stage Credit Check is deleted, but milestones CCS and CCU are to be retained. In this case, the sentry of CCS will become “IDGS $\wedge \ 9 \ge 8$”, and the sentry of $\textsf {CCU}$ will become “IDGS $\wedge 9 < 8$”.    $\square$

Suppose that $\mathcal{F}$ is the set of milestones and stages whose sentries are impacted by the stage deletion, if $\overrightarrow{c}$ is a vector of constants having the types of $\overrightarrow{a} = {\textit{sig}}_{{\textit{out}}}(S)$, and let $\varOmega$ be “$\overrightarrow{a} = \overrightarrow{c}$”. Then $\varGamma {\rightleftharpoons _{\varOmega ,\mathcal{F}}} {\textit{del}}(\varGamma ,m)$.

We now state a general result concerning deletion of a set $\mathcal{X}$ of stages and milestones. Let $\overrightarrow{a}/\overrightarrow{c}$ be the union of all the mappings from attributes to constants (used for the stages that are deleted). The delete operators above can be applied one at a time for the elements of $\mathcal{X}$, and the ordering does not affect the end result, denoted as ${\textit{del}}(\varGamma , \mathcal{X}, \overrightarrow{a}/\overrightarrow{c})$.

Theorem 5.6

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$, $\mathcal{X}$, $\overrightarrow{a}$ and $\overrightarrow{c}$ and $\varGamma ' = del(\varGamma , \mathcal{X}, \overrightarrow{a}/\overrightarrow{c})$ be as above. Let $\mathcal{F}$ be the collection of all stages and milestones in $\varGamma '$ whose sentries have been modified, and let $\varOmega$ be the formula $\overrightarrow{a} = \overrightarrow{c}$. Then $\varGamma {\rightleftharpoons _{\varOmega ,\mathcal{F}}} \varGamma '$. Furthermore, if $\mathcal{O}\subseteq {\textit{Att}}_{{\textit{out}}}$ is completion-independent modulo $\mathcal{F}$, then $\varGamma {\rightleftharpoons _{\varOmega ,\mathcal{O}}} \varGamma '$.

5.2 Insertion

This subsection studies property preservation in the context of insertions to an FA-GSM schema $\varGamma$. Speaking intuitively, the emphasis here is on enabling the designer to insert one or several stages and milestones, while ensuring that the global impact of the insertion is minimized “when things go right” (cf. schema ${\textsf {BCA}}^{ins}$).

The following definition is provided to talk about “bulk” insertions.

Definition 5.7

Let $\varGamma$ be an FA-GSM schema. An insertable fragment for $\varGamma$ is a tuple $\varDelta = ({\textit{Att}}^\varDelta = {\textit{Att}}_d^\varDelta \cup {\textit{Att}}_m^\varDelta \cup {\textit{Att}}_{\textit{S}}^\varDelta , {\textit{Att}}_{{\textit{out}}}^\varDelta , {\textit{sen}}^\varDelta , {\textit{sig}}^\varDelta )$ where the set ${\textit{Att}}^\varDelta$ are new, where the sentries of $\varDelta$ may refer to attributes from $\varGamma$ and $\varDelta$, and where the insertion of $\varDelta$ into $\varGamma$ yields a well-formed FA-GSM schema.

To enable modular insertions, and to facilitate straightforward reasoning about the impact of an insertion, a best practice is to include as part of $\varDelta$ one or more milestones that are used to indicate the “success” or “failure” of a case with regards to the inserted activity. The following result assumes there is a single “success” milestone. The result follows easily from the Lifting Lemma.

Theorem 5.8

Let $\varGamma = ({\textit{Att}}= {\textit{Att}}_d \cup {\textit{Att}}_m \cup {\textit{Att}}_{\textit{S}}, {m_\mathrm{\small start}}, {\textit{Att}}_{{\textit{out}}}, {\textit{sen}}, {\textit{sig}})$ be an FA-GSM schema, and let $\varDelta = ({\textit{Att}}^\varDelta = {\textit{Att}}_d^\varDelta \cup {\textit{Att}}_m^\varDelta \cup {\textit{Att}}_{\textit{S}}^\varDelta , {\textit{Att}}_{{\textit{out}}}^\varDelta , {\textit{sen}}^\varDelta , {\textit{sig}}^\varDelta )$ be an insertable fragment that includes a milestone ${m_{{\small success}}}$. Suppose that $\mathcal{F}\subseteq {\textit{Att}}_m$ is a family of milestones in $\varGamma$, and suppose that $\varGamma '$ is the result of modifying ${\textit{ins}}(\varGamma ,\varDelta )$ by replacing each sentry $\mu$ of a milestone in $\mathcal{F}$ by $\mu \wedge {m_{{\small success}}}$. Let $\varOmega$ = “${m_{{\small success}}}$”. Finally, let $\mathcal{O}\subseteq {\textit{Att}}_{{\textit{out}}}$ be completion-independent modulo $\mathcal{F}$ in $\varGamma '$. Then $\varGamma {\rightharpoonup _{\varOmega ,\mathcal{O}}} \varGamma '$.

Example 5.9

In the schema ${\textsf {BCA}}^{ins}$ of Example 2.4, with regards to the above theorem, the milestone AMCS plays the role of ${m_{{\small success}}}$, the set {PCS} plays the role of $\mathcal{F}$, and the set {recommendation, DCS, DCU} plays the rols of $\mathcal{O}$. In this case, the theorem tells us that for each execution of ${\textsf {BCA}}^{ins}$ for which AMCS goes true, there is a corresponding execution of the base schema ${\textsf {BCA}}^{base}$ with the same outcomes on $\mathcal{O}$.    $\square$

6 Related Work

We discuss the literature on changes in process models for activity-centric business process management and case management.

In the context of activity-centric BPM, change operations have been proposed [26]. Different correctness criteria have been identified in the literature to assess which changes are allowed so that cases can be migrated properly from an old to a new schema [24]. A particular focus has been on ensuring that when the execution of a BP instance starts on one schema and migrates to another one while in flight, the final BP instance corresponds to an execution of the new schema. In our approach, we study a novel form of correctness, which focuses on preservation of schema properties, defined in terms of emulatability of one shema by another one. A form of unconditional emulatability was studied in connection with declarative artifact-centric business processes in [4]. That work was in an abstract setting; in contrast the results here are tied to a practical Case Management model, and motivated by a real-world use case.

Case management originates from industry, including, e.g., [25] and work on business artifacts, e.g., [22]. Recent overview works include [8, 13, 20]. Case management is related to the more general concept of data-centric business process management, which studies how activity-centric processes can be made more data-aware [16, 18, 22, 23] to improve their flexibility. This includes work on declarative artifact-centric models, including GSM [5, 6] and declarative process models for case management [12].

Though the problem of change has been recognized as central to case management [13], in particular adaptive case management [19], it has not been widely studied. Mukkalama et al. [21] study change in DCR Graphs, a declarative formalism for case management. They define basic change operations that add and remove behavior, but their operations are aimed at a micro-level, so removing atomic elements from schema. In our approach, we study also the impact of adding and removing larger fragments, so at a macro level. They focus on logical correctness and the use of automated verification techniques, whereas we develop tests for property preservation that can be checked at a syntactic level.

Motahari et al. [19] present a framework and prototype implementation that supports adaptive case management in social enterprises. The framework supports change, but does not address preservation of properties across changes.

There has been active research on verification for artifact-centric BPM models (e.g., [1, 2, 7, 11]). That work could be also be applied to reason about preservation of properties of case management schemas during evolution. The approach in the current paper uses syntactic conditions rather than semantic ones, and would thus be subsantially easier to deploy and maintain than a verification-based approach.

7 Conclusion

This paper studies schema modifications in the context of a varient of the Guard-Stage-Milestone (GSM) model for Case Management. The main contributions of this paper are (i) a precise definition for testing the preservation of properties through the use of conditional emulatability; (ii) the development of a general-purpose “Lifting Lemma” which allows a variety of approaches to achieve and/or prove property preservation; and (iii) the specification of operators to perform schema manipulations that are guaranteed to preserve certain properties. The theoretical work is motivated by examples arising in a real-world application.

The research here can be extended in several directions, including the following: (a) extend results to more general kinds of GSM schema; (b) extend results to other Case Management and BPM models ([25] is a natural first candidate, and also the OMG CMMN standard [3]); (c) develop algorithms for schema modifications other than deletion and insertion, that preserve specified properties; (d) generalize to support adaptation of schemas for cases that are “in-flight”. and (e) develop approaches to apply the theoretical results developed here in practical settings.