disjunction $\lor$. Thus, in PQL, expression $\neg(a\lor b\land c)\lor d\land
e$ is evaluated as $(\neg(a\lor(b\land c)))\lor(d\land e)$.

One can test whether a predicate evaluates to _true_ or _false_ as follows.

$\displaystyle\begin{split}M_{\texttt{LogicalTest}}[p:\texttt{LogicalTest},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\;M_{\texttt{Predicate}}(p.\mathit{pred},s,\mathit{vals})&p\,\,\,\textbf{{is}}\,\,\,\texttt{IsTrue}\lor
p\,\,\,\textbf{{is}}\,\,\,\texttt{IsNotFalse}\\\
\;\neg\,\,M_{\texttt{Predicate}}(p.\mathit{pred},s,\mathit{vals})&p\,\,\,\textbf{{is}}\,\,\,\texttt{IsFalse}\lor
p\,\,\,\textbf{{is}}\,\,\,\texttt{IsNotTrue}\\\ \end{cases}$

The TaskInSetOfTasks construct tests if a task is a member of a set of tasks.

$\displaystyle\begin{split}M_{\texttt{TaskInSetOfTasks}}[p:\texttt{TaskInSetOfTasks},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$ $\displaystyle
M_{\texttt{Task}}(p.\mathit{task})\;\in\;M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals})$

Every specimen of SetComparison denotes a set comparison operation.888As the
meaning of a SetOfTasks construct is a set composed of the meanings of all and
only its Task elements, each interpreted as a set of character strings, the
identity of elements is defined as set equality over sets of character
strings.

$\displaystyle\begin{split}M_{\texttt{SetComparison}}\\\
[p:\texttt{SetComparison},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\;\begin{split}M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vals})=\;\;\;\;\;\;\;\;\;\;\\\
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vals})\;\;\;\;\;\;\;\;\;\;\end{split}&\begin{split}p.\mathit{oper}\,\,\,\textbf{{is}}\;\;\;\\\
\texttt{Identical}\end{split}\\\\[9.00002pt]
\;\begin{split}M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vals})\neq\\\
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vals})\end{split}&\begin{split}p.\mathit{oper}\,\,\,\textbf{{is}}\;\;\;\\\
\texttt{Different}\end{split}\\\\[9.00002pt]
\;\begin{split}M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vals})\,\,\cap\\\
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vals})\neq\emptyset\end{split}&\begin{split}p.\mathit{oper}\,\,\,\textbf{{is}}\;\;\;\;\;\;\;\;\;\;\;\\\
\texttt{OverlapsWith}\end{split}\\\\[9.00002pt]
\;\begin{split}M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vals})\,\,\subseteq\\\
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vals})\end{split}&\begin{split}p.\mathit{oper}\,\,\,\textbf{{is}}\;\\\
\texttt{SubsetOf}\end{split}\\\\[9.00002pt]
\;\begin{split}M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vals})\,\,\subset\\\
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vals})\end{split}&\begin{split}p.\mathit{oper}\,\,\,\textbf{{is}}\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\\\
\texttt{ProperSubsetOf}\end{split}\\\ \end{cases}$

The denotation of a specimen of UnaryPredicate is a unary behavioral relation.

$\displaystyle\begin{split}M_{\texttt{UnaryPredicate}}[p:\texttt{UnaryPredicate},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\;\mathit{canOccur(s,M_{\texttt{Task}}(p.\mathit{task}))}&p.\mathit{name}\,\,\,\textbf{{is}}\,\,\,\texttt{CanOccur}\\\
\;\mathit{alwaysOccurs(s,M_{\texttt{Task}}(p.\mathit{task}))}&p.\mathit{name}\,\,\,\textbf{{is}}\,\,\,\texttt{AlwaysOccurs}\end{cases}$

Note that the respective behavioral relation is computed for the system that
is being matched to the query. Similarly, the meaning of a specimen of
BinaryPredicate is a binary behavioral relation.

$\displaystyle\begin{split}M_{\texttt{BinaryPredicate}}\\\
[p:\texttt{BinaryPredicate},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\;\begin{split}\mathit{canConflict}(s,M_{\texttt{Task}}(p.\mathit{task}_{1}),\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\\\
M_{\texttt{Task}}(p.\mathit{task}_{2}))\;\;\;\;\;\;\;\;\;\end{split}&\begin{split}p.\mathit{name}\,\,\,\textbf{{is}}\;\;\;\;\;\;\;\\\
\texttt{CanConflict}\end{split}\\\\[9.00002pt]
\;\begin{split}\mathit{canCooccur}(s,M_{\texttt{Task}}(p.\mathit{task}_{1}),\;\;\;\;\;\;\,\\\
M_{\texttt{Task}}(p.\mathit{task}_{2}))\end{split}&\begin{split}p.\mathit{name}\,\,\,\textbf{{is}}\;\;\;\;\\\
\texttt{CanCooccur}\end{split}\\\\[9.00002pt]
\;\begin{split}\mathit{conflict}(s,M_{\texttt{Task}}(p.\mathit{task}_{1}),\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\\\
M_{\texttt{Task}}(p.\mathit{task}_{2}))\end{split}&\begin{split}p.\mathit{name}\,\,\,\textbf{{is}}\\!\\!\\\
\texttt{Conflict}\end{split}\\\\[9.00002pt]
\;\begin{split}\mathit{cooccur}(s,M_{\texttt{Task}}(p.\mathit{task}_{1}),\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\\\
M_{\texttt{Task}}(p.\mathit{task}_{2}))\end{split}&\begin{split}p.\mathit{name}\,\,\,\textbf{{is}}\\!\\!\\!\\!\\!\\!\\!\\\
\texttt{Cooccur}\end{split}\\\\[9.00002pt]
\;\begin{split}\mathit{totalCausal}(s,M_{\texttt{Task}}(p.\mathit{task}_{1}),\;\;\;\;\;\;\;\;\,\\\
M_{\texttt{Task}}(p.\mathit{task}_{2}))\end{split}&\begin{split}p.\mathit{name}\,\,\,\textbf{{is}}\;\;\;\;\;\;\;\\\
\texttt{TotalCausal}\end{split}\\\\[9.00002pt]
\;\begin{split}\mathit{totalConcurrent}(s,M_{\texttt{Task}}(p.\mathit{task}_{1}),\\\
M_{\texttt{Task}}(p.\mathit{task}_{2}))\end{split}&\begin{split}p.\mathit{name}\,\,\,\textbf{{is}}\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\\\
\texttt{TotalConcurrent}\end{split}\\\ \end{cases}$

As of today, PQL offers two unary and six binary behavioral predicates, refer
to Section 4.1.3. We expect that future studies will justify the use of other
behavioral predicates for process querying, which consequently will result in
the introduction of new predicates in PQL, ultimately improving its
expressiveness. The reader can refer to Section 4.6 to learn about methods for
computing the PQL predicates (both unary and binary predicates).

As already mentioned, PQL utilizes a well-known mechanism of macros to combine
results of several unary or binary relations. A specimen of
UnaryPredicateMacro combines several results of unary behavioral relations
using existential and universal quantifiers as follows.

$\displaystyle\begin{split}M_{\texttt{UnaryPredicateMacro}}\\\
[p:\texttt{UnaryPredicateMacro},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\begin{split}\;\exists\,\,t\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals}):\\\
\mathit{canOccur}(s,t)\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\,\,\,\texttt{CanOccur})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{Any})\end{split}\\\\[9.00002pt]
\begin{split}\;\forall\,t\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals}):\\\
\mathit{canOccur}(s,t)\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\,\,\,\texttt{CanOccur})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{All})\end{split}\\\\[9.00002pt]
\begin{split}\;\exists\,\,t\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals}):\\\
\mathit{alwaysOccurs}(s,t)\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\,\,\,\texttt{AlwaysOccurs})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{Any})\end{split}\\\\[9.00002pt]
\begin{split}\;\forall\,t\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals}):\\\
\mathit{alwaysOccurs}(s,t)\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\,\,\,\texttt{AlwaysOccurs})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{All})\end{split}\\\\[9.00002pt]
\end{cases}$

For example, a specimen $p$ of UnaryPredicateMacro such that $p.\mathit{name}$
is of type AlwaysOccurs and $p.q$ is of type All denotes the truth value of
_true_ in the context of system $s$ iff for every task $t$ in the set of tasks
defined by $p.\mathit{tasks}$ it holds that $t$ occurs in every instance of
$s$.

PQL offers two types of binary predicate macros: macros that relate a task to
a set of tasks, and macros that relate two sets of tasks. One can use a
specimen of the BinaryPredicateMacroTaskSet construct to test if a task is in
a binary behavioral relation with some (or all) tasks in a given set.

$\displaystyle\begin{split}M_{\texttt{BinaryPredicateMacroTaskSet}}\\\
[p:\texttt{BinaryPredicateMacroTaskSet},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\begin{split}\;\exists\,\,t\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals}):\;\;\;\;\;\;\;\\\
\mathit{canConflict}(s,M_{\texttt{Task}}(p.\mathit{task}),t)\;\;\;\;\;\;\;\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\\\
\texttt{CanConflict})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{Any})\end{split}\\\\[22.50003pt]
\begin{split}\;\forall\,t\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks},s,\mathit{vals}):\\\
\mathit{canConflict}(s,M_{\texttt{Task}}(p.\mathit{task}),t)\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\\\
\texttt{CanConflict})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{All})\end{split}\\\
\;\;\;\ldots&\end{cases}$

We only specify the denotation of a specimen $p$ for which it holds that
$p.\mathit{name}$ is of type CanConflict. Note that the denotations of
specimens for other binary predicate names are defined analogously. E.g., one
can use a specimen $p$ of BinaryPredicateMacroTaskSet such that
$p.\mathit{name}$ is of type TotalCausal and $p.q$ is of type All to check if
the task defined by $p.\mathit{task}$ is in the TotalCausal behavioral
relation with every task in the set of tasks defined by $p.\mathit{tasks}$,
etc.

Finally, the denotation of a specimen of BinaryPredicateMacroSetSet is as
follows.

$\displaystyle\begin{split}M_{\texttt{BinaryPredicateMacroSetSet}}\\\
[p:\texttt{BinaryPredicateMacroSetSet},\\\
s:\mathbb{S},\mathit{vals}:\powerset{(\mathbb{V}\times\powerset{(\mathbb{T})})}]\end{split}$
$\displaystyle\triangleq$
$\displaystyle\begin{cases}\begin{split}\;\exists\,t_{1}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vs})\;\;\;\;\;\;\;\\\
\exists\,t_{2}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vs}):\;\;\;\;\;\;\;\\\
\mathit{canConflict}(s,t_{1},t_{2})\;\;\;\;\;\;\;\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\\\
\texttt{CanConflict})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{Any})\end{split}\\\\[22.50003pt]
\begin{split}\;\exists\,t_{1}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vs})\;\;\;\;\;\;\;\\\
\forall\,t_{2}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vs}):\;\;\;\;\;\;\;\\\
\mathit{canConflict}(s,t_{1},t_{2})\;\;\;\;\;\;\;\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\\\
\texttt{CanConflict})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{Some})\end{split}\\\\[22.50003pt]
\begin{split}\;\forall\,t_{1}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vs})\\\
\exists\,t_{2}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vs}):\\\
\mathit{canConflict}(s,t_{1},t_{2})\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\\\
\texttt{CanConflict})\,\land\\\
(p.q\,\,\,\textbf{{is}}\,\,\,\texttt{Each})\end{split}\\\\[22.50003pt]
\begin{split}\;\forall\,t_{1}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{1},s,\mathit{vs})\\\
\forall\,t_{2}\in
M_{\texttt{SetOfTasks}}(p.\mathit{tasks}_{2},s,\mathit{vs}):\\\
\mathit{canConflict}(s,t_{1},t_{2})\end{split}&\begin{split}(p.\mathit{name}\,\,\,\textbf{{is}}\\\
\texttt{CanConflict})\,\land\\\ (p.q\,\,\,\textbf{{is}}\,\,\,\texttt{All})\\\
\end{split}\\\ \;\;\ldots&\end{cases}$

Again, for space considerations, we omit the precise definitions of
denotations of all specimens of the BinaryPredicateMacroSetSet construct. Note
that the missing definitions are similar to those shown above for a specimen
$p$ for which $p.\mathit{name}$ is of type CanConflict. For example, one can
use a specimen $p$ of BinaryPredicateMacroSetSet such that $p.\mathit{name}$
is of type conflict and $p.q$ is of type Any to check if some task in the set
of tasks defined by $p.\mathit{tasks}_{1}$ is in the Conflict behavioral
relation with some task in the set of tasks defined by $p.\mathit{tasks}_{2}$,
etc.

In Table LABEL:tab:semantics:Q3, we detail the meaning of query _Q3_ from
Section 2 matched to the model in Figure LABEL:fig:EPC. In the table, the
numbers in the first column refer to nodes in the abstract syntax tree in
Figure 3, e.g., number 1 in the first column refers to node “Task (1)” in the
figure. The second column contains denotations of the corresponding
constructs, while the third column contains further comments.

Table 5. Meaning of the example PQL query _Q3_ in Section 2 explained using Figure 3. No. |  Denotation |  Comment
---|---|---
1 |  $\\{$“Start inventory recount”$\\}$ |  This is a specimen of ExactTask and, thus, it denotes a singleton of its label.
2 |  $\\{$“No variance is determined”$\\}$ |  This is a specimen of ExactTask and, thus, it denotes a singleton of its label.
3 |  $\\{\\{$“Start inventory recount”$\\}$, $\\{$“No variance is determined”$\\}\\}$ |  This set of tasks is specified as a fixed value composed of tasks denoted by 1 and 2.
4 |  $(x,\\{\\{$“Start inventory recount”$\\}$, $\\{$“No variance is determined”$\\}\\})$ |  This variable associates symbolic name $x$ with the set of tasks denoted by $3$.
5 |  $\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}$ |  This is a specimen of DefSimTask and, thus, denotes the set of all labels in the repository that are similar to its label.
6 |  $\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}\\}$ |  This set of tasks is specified as a fixed value composed of the task denoted by 5.
7 |  $(y,\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}\\})$ |  This variable associates symbolic name $y$ with the set of tasks denoted by $6$.
8 |  $\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}\\}$ |  This set of tasks is specified as the value associated by 7 with symbolic name $y$.
9 |  $\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}$ |  This is a specimen of DefSimTask and, thus, denotes the set of all labels in the repository that are similar to its label.
10 |  $\\{\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}\\}$ |  This set of tasks is specified as a fixed value composed of the task denoted by 9.
11 |  $\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}$, $\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}\\}$ |  This set of tasks is computed as the union of sets denoted by 8 and 10.
12 |  $(z,\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}$, $\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}\\})$ |  This variable associates symbolic name $z$ with the set of tasks denoted by $11$.
13 |  $\\{\\{$“Storage type is to be blocked for inventory”$\\}$, $\\{$“Storage type block”$\\}$, $\\{$“Storage type is blocked”$\\}$, $...\,\,\\}$ |  This set of tasks is defined by all the labels in the model from Figure LABEL:fig:EPC; each function and event defines one PQL task in the set.
14 |  $\\{\\{$“Storage bin is blocked”$\\}$, $\\{$“System inventory record is created”$\\}$, $\\{$“Physical inventory is active”$\\}$, $\\{$“Print inventory list”$\\}$, $\\{$“Physical inventory list is printed”$\\}$, $\\{$“Enter count results”$\\}\\}$ |  The set of tasks from the set denoted by 13 that occur in every instance of the model in Figure LABEL:fig:EPC; the checks are performed on the workflow system in Figure LABEL:fig:system using the result of Lemma 4.11.
15 |  $(w,\\{\\{$“Storage bin is blocked”$\\}$, $\\{$“System inventory record is created”$\\}$, $\\{$“Physical inventory is active”$\\}$, $\\{$“Print inventory list”$\\}$, $\\{$“Physical inventory list is printed”$\\}$, $\\{$“Enter count results”$\\}\\})$ |  This variable associates symbolic name $z$ with the set of tasks denoted by $14$.
16 |  $\\{(x,\\{\\{$“Start inventory recount”$\\}$, $\\{$“No variance is determined”$\\}\\})$, … $\\}$ |  The set contains values of all the variables used in the query, i.e., it contains denotations of 4, 7, 12, and 15.
17 |  $\mathbb{A}$ |  All the attribute names used in the repository.
18 |  $\\{/\texttt{SAP-R3-EPC-Repo}\\}$ |  The set composed of one location specified by the location path "/SAP-R3-EPC-Repo".
19 |  $\\{\\{$“Start inventory recount”$\\}$, $\\{$“No variance is determined”$\\}\\}$ |  This set of tasks is specified as the value associated by 4 with symbolic name $x$.
20 |  $\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}$, $\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}\\}$ |  This set of tasks is specified as the value associated by 12 with symbolic name $z$.
21 |  $\\{\\{$“Start inventory recount”$\\}$, $\\{$“No variance is determined”$\\}$, $\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}$, $\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}\\}$ |  This set of tasks is computed as the union of sets denoted by 19 and 20.
22 |  $\mathit{true}$; every task in the set denoted by 21 occurs in at least one instance of the model in Figure LABEL:fig:EPC. |  The checks are performed on the workflow system in Figure LABEL:fig:system using the result of Lemma 4.9.
23 |  $\\{$“Start inventory recount”$\\}$ |  This is a specimen of ExactTask and, thus, it denotes a singleton of its label.
24 |  $\\{\\{$“Storage bin is blocked”$\\}$, $\\{$“System inventory record is created”$\\}$, $\\{$“Physical inventory is active”$\\}$, $\\{$“Print inventory list”$\\}$, $\\{$“Physical inventory list is printed”$\\}$, $\\{$“Enter count results”$\\}\\}$ |  This set of tasks is specified as the value associated by 15 with symbolic name $w$.
25 |  $\mathit{false}$ |  The task denoted by 23 is not a member of the set of tasks denoted by 24.
26 |  $\mathit{true}$ |  Negation of denotation of 25.
27 |  $\\{$“No variance is determined”$\\}$ |  This is a specimen of ExactTask and, thus, it denotes a singleton of its label.
28 |  $\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}\\}$ |  This set of tasks is specified as the value associated by 8 with symbolic name $y$.
29 |  $\mathit{true}$; the task denoted by 27 is in conflict with every task in the set denoted by 28. |  The checks are performed on the workflow system in Figure LABEL:fig:system based on Definition 4.7 using the technique proposed in (Polyvyanyy et al., 2014b).
30 |  $\\{$“Start inventory recount”$\\}$ |  This is a specimen of ExactTask and, thus, it denotes a singleton of its label.
31 |  $\\{\\{$“Clear differences”, “Clear differences WM”, “Clear differences IM”$\\}$, $\\{$“Difference is posted”, “Difference is posted to interface”, “Difference is posted to IM”$\\}\\}$ |  This set of tasks is specified as the value associated by 12 with symbolic name $z$.
32 |  $\mathit{true}$; the task denoted by 30 is in the total causal relation with every task in the set denoted by 31. |  The checks are performed on the workflow system in Figure LABEL:fig:system based on Definition 4.7 using the technique proposed in (Polyvyanyy et al., 2014b).
33 |  $\mathit{true}$ |  Conjunction of denotations of 22, 26, 29, and 32.
34 |  $\\{(s,\\{($Author, SAP$),...\\}),...\\}$ |  A result of query _Q3_ from Section 2.

Thus, the meaning of _Q3_ is a set of pairs, where the first element of each
pair is a model nested in a location from the set denoted by 18 and the second
element is the set of attribute-value pairs for the attribute names contained
in the set denoted by 17. In Table LABEL:tab:semantics:Q3, $s$ in row 34 is
the system in Figure LABEL:fig:system.

###  4.6. Denotations of Basic Predicates

This section presents denotations of the basic PQL predicates and techniques
for computing them.

####  4.6.1. Definitions of the PQL Predicates

Note that all the subsequent discussions are restricted to workflow systems.
Before providing denotations of the predicates over PQL tasks, as demanded by
the dynamic semantics of PQL, refer to Section 4.5, we give definitions of the
PQL predicates over character strings.

Predicates over character strings. Given a workflow system, the
$\mathit{canOccur}$ and $\mathit{alwaysOccurs}$ unary predicates on an input
character string are defined below.

###### Definition 4.2 (Can occur and always occurs).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system and let $x\in\mathbb{C}$ be a
non-empty character string.

  * $\circ$

$x$ _can occur_ in $S$, denoted by $\mathit{canOccur}(S,x)$, iff there is a
label execution $\eta$ of $S$ such that $x\in\eta$.

  * $\circ$

$x$ _always occurs_ in $S$, denoted by $\mathit{alwaysOccurs}(S,x)$, iff for
every label execution $\eta$ of $S$ it holds that $x\in\eta$.999Given a
sequence $\sigma$, $x\in\sigma$ denotes the fact that $x$ is an element of
$\sigma$. $\lrcorner$

Hence, a character string $x\in\mathbb{C}$ can occur in a workflow system $S$
iff one can observe $x$ in some execution of $S$, i.e., an activity denoted by
$x$ can be performed in some business scenario captured in $S$. In turn, $x$
always occurs in $S$, iff it is observed in every execution of $S$.

As already mentioned, the binary predicates of PQL are grounded in the
behavioral relations of the 4C spectrum. In (Polyvyanyy et al., 2014b), the
authors define the 4C spectrum on systems in which transitions have distinct
labels and then extend those relations to the general case when the same label
can be assigned to several transitions in the system. The PQL predicates are
grounded in these generalized relations. Thus, the $\mathit{canConflict}$ and
$\mathit{canCooccur}$ predicates are defined as follows.

###### Definition 4.3 (Basic conflict and co-occurrence).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system and let $x,y\in\mathbb{C}$ be
two non-empty character strings.

  * $\circ$

$x$ _can conflict with_ $y$ in $S$, denoted by $\mathit{canConflict}(S,x,y)$,
iff there is a label execution $\eta$ of $S$ such that $x\in\eta$ and
$y\not\in\eta$.

  * $\circ$

$x$ and $y$ _can co-occur_ in $S$, denoted by $\mathit{canCooccur}(S,x,y)$,
iff there is a label execution $\eta$ of $S$ such that $x\in\eta$ and
$y\in\eta$. $\lrcorner$

Intuitively, $x$ can conflict with $y$ iff there exists an execution of $S$
which performs $x$ but not $y$, whereas $x$ and $y$ can co-occur iff they both
can be observed in some execution of $S$.

The 4C spectrum uses the basic conflict and co-occurrence relations as
building blocks to define several other relations, two of which are among the
selected PQL predicates.

###### Definition 4.4 (Conflict and co-occurrence).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system and let $x,y\in\mathbb{C}$ be
two non-empty character strings.

  * $\circ$

$x$ and $y$ are in _conflict_ in $S$, denoted by $\mathit{conflict}(S,x,y)$,
iff
$\mathit{canConflict}(S,x,y)\;\land\;\mathit{canConflict}(S,y,x)\;\land\;\neg\;\mathit{canCooccur}(S,x,y)$.

  * $\circ$

$x$ and $y$ _co-occur_ in $S$, denoted by $\mathit{cooccur}(S,x,y)$, iff
$\neg\;\mathit{canConflict}(S,x,y)\;\land\;\neg\;\mathit{canConflict}(S,y,x)\;\land\;\mathit{canCooccur}(S,x,y)$.
$\lrcorner$

Accordingly, $x$ and $y$ are in conflict in $S$ iff they cannot co-occur but
can conflict with each other, i.e., they can be observed in some executions of
$S$, but never together in the same execution. In contrast, $x$ and $y$ co-
occur in $S$ iff they can co-occur but cannot conflict, i.e., they can be
observed together in some executions of $S$, $x$ is never observed in an
execution that does not include an occurrence of $y$, and $y$ is never
observed in an execution that does not include an occurrence of $x$.

Figure 4. A workflow system.

To give an example, consider the workflow system $S$ in Figure 4. For this
system, the expression
$\mathit{canOccur(S,\texttt{a}^{\prime})}\land\neg\;\mathit{alwaysOccurs(S,\texttt{a}^{\prime})}$
evaluates to _true_. Indeed, there exists a label execution
$\eta_{1}:=\left\langle\texttt{a}^{\prime},\texttt{b},\texttt{c},\texttt{d},\texttt{e}\right\rangle$
of $S$ that justifies the fact that $\texttt{a}^{\prime}$ can occur in $S$,
and a label execution
$\eta_{2}:=\left\langle\texttt{a}^{\prime\prime},\texttt{b},\texttt{c},\texttt{d},\texttt{e}\right\rangle$
of $S$ that justifies the fact that $\texttt{a}^{\prime}$ does not always
occur in $S$. Note that strings b, c, d, and e, always occur in $S$ as they
are present in all of the four label executions of $S$. Furthermore, both
$\mathit{canConflict}(S,\texttt{b},\texttt{a}^{\prime})$ and
$\mathit{canCooccur}(S,\texttt{b},\texttt{a}^{\prime})$ evaluate to _true_ ,
because b can be observed without $\texttt{a}^{\prime}$, for example in
$\eta_{2}$, and with $\texttt{a}^{\prime}$, for example in $\eta_{1}$. Note
that a and $\texttt{a}^{\prime}$ are in conflict, i.e.,
$\mathit{conflict}(S,\texttt{a},\texttt{a}^{\prime})$ evaluates to _true_ , as
these two strings are never observed together. Finally, b and e are example
strings that co-occur in $S$, i.e.,
$\mathit{cooccur}(S,\texttt{b},\texttt{e})$ evaluates to _true_.

Executions of workflow systems capture orderings of transition occurrences.
One can rely on _processes_ to adequately represent _causality_ and
_concurrency_ relations on transition occurrences (Goltz and Reisig, 1983).

###### Definition 4.5 (Process).

A _process_ of a system $S:=(P,T,F,\lambda,M)$ is a 4-tuple
$\pi:=(B,E,G,\rho)$, where $B$ is a set of _conditions_ , $E$ is a set of
_events_ , $G\subseteq(B\times E)\cup(E\times B)$ is the _flow relation_ ,
such that $G^{+}$ is irreflexive and $\forall\,b\in B:|\\{e\in
E\\!\divides\\!(e,b)\in G\\}|\leq 1\;\land\;|\\{e\in E\\!\divides\\!(b,e)\in
G\\}|\leq 1$, and $\rho:B\cup E\rightarrow P\cup T$ is such that:

  * $\circ$

$\rho(B)\subseteq P$ and $\rho(E)\subseteq T$, i.e., $\rho$ preserves the
nature of nodes,

  * $\circ$

$\forall\,b_{1},b_{2}\in\mathit{Min}(\pi):(b_{1},b_{2})\not\in
G^{+}\land(b_{2},b_{1})\not\in G^{+}$, $\forall\,b_{1}\in
B\setminus\mathit{Min}(\pi)\exists\,b_{2}\in\mathit{Min}(\pi):(b_{2},b_{1})\\!\in
G^{+}$, and $\forall p\in P:M(p)=|\rho^{-1}(p)\cap\mathit{Min}(\pi)|$, i.e.,
$\pi$ starts at $M$, and

  * $\circ$

for every event $e\in E$ and for every place $p\in P$ it holds that
$|\\{(p,t)\in F\\!\divides\\!t=\rho(e)\\}|=|\rho^{-1}(p)\cap\bullet{e}\,|$ and
$|\\{(t,p)\in F\\!\divides\\!t=\rho(e)\\}|=|\rho^{-1}(p)\cap{e\\!}\bullet|$,
i.e., $\rho$ respects the environment of transitions.101010$R^{+}$ denotes the
transitive closure of a binary relation
$R$.111111$f(X):=\\{f(x)\\!\divides\\!x\in X\\}$ and $f^{-1}(z):=\\{y\in
Y\\!\divides\\!f(y)=z\\}$, where $X$ is a subset of $f$’s domain
$Y$.121212$\mathit{Min}(\pi):=\\{b\in B\\!\divides\\!\forall e\in
E:(e,b)\not\in G\\}$.131313$\bullet{e}:=\\{b\in B\\!\divides\\!(b,e)\in G\\}$
and ${e}\bullet:=\\{b\in B\\!\divides\\!(e,b)\in G\\}$. $\lrcorner$

A process of a Petri net system is an acyclic bipartite graph, in which
conditions and events are two disjoint sets of nodes, and a mapping from nodes
of the process to nodes of the system. Figure 5 shows three processes of the
system in Figure 4. Conditions and events of a process are drawn as places and
transitions, respectively. The labels in the figures encode mappings of nodes
of processes to nodes of the system. In particular, each condition $b_{i}$
maps to place $p_{i}$, $i\in[1..7]$, and each event $e_{j}$ maps to transition
$t_{j}$, $j\in[1..6]$. In general, several conditions (events) of a process
can refer to the same place (transition) of the corresponding system. For
example, there exist processes of the system in Figure LABEL:fig:system in
which several conditions and several events refer to the same place and
transition, respectively. These are the processes that describe multiple
occurrences of transitions in the loop with entry place $c_{4}$ and exit place
$c_{5}$.

Figure 5. Three processes of the system in Figure 4.

Given a process $\pi$ of a system $S$, by $E_{\pi}$ and $\rho_{\pi}$ we refer
to events of $\pi$ and the function that maps nodes of $\pi$ to nodes of $S$,
respectively. A process $\pi$ of $S$ can be interpreted as a collection of
occurrence sequences of $S$, where every event $e\in E_{\pi}$ describes an
occurrence of transition $\rho_{\pi}(e)$. For example, the process in Figure 5
describes a single occurrence sequence of the system in Figure 4, namely
$\left\langle t_{1},t_{3},t_{5}\right\rangle$, whereas the process in Figure 5
describes two occurrence sequences of the system in Figure 4, namely
$\left\langle t_{1},t_{3},t_{4},t_{5},t_{6}\right\rangle$ and $\left\langle
t_{1},t_{3},t_{5},t_{4},t_{6}\right\rangle$. Given a workflow system $S$, by
$\Pi_{S}$ we denote the set that contains all and only processes of $S$ (up to
isomorphism) that describe all the executions of $S$. Note that the set of all
processes of a workflow system can be infinite. For example, the set of all
processes of the system in Figure LABEL:fig:system that describe all its
executions is infinite. Let $S$ be the workflow system in Figure 4. Then,
$\Pi_{S}$ is composed of the two processes shown in Figs. 5 and 5; these two
processes describe all the four executions of the system. Note that the
process from Figure 5 is not in $\Pi_{S}$ because the occurrence sequence it
describes is not an execution of $S$. Finally, by $\Delta_{S}(x,y)$, where
$x,y\in\mathbb{C}$, we refer to the set
$\\{\pi\in\Pi_{S}\\!\divides\\!\exists\,e_{1},e_{2}\in
E_{\pi}:\lambda(\rho_{\pi}(e_{1}))=x\;\land\;\lambda(\rho_{\pi}(e_{2}))=y\\}$,
i.e., the set that consists of every process from $\Pi_{S}$ which contains an
event that describes an occurrence of a transition with label $x$ and an event
that describes an occurrence of a transition with label $y$.

Processes of systems can be characterized by the causality and concurrency
relations over their nodes (Nielsen et al., 1981; Goltz and Reisig, 1983). An
event $e_{1}\in E_{\pi}$ _causes_ event $e_{2}\in E_{\pi}$ of a process $\pi$,
denoted by $e_{1}\rightarrowtail_{\pi}e_{2}$, iff $(e_{1},e_{2})\in G^{+}$.
Two events $e_{1}\in E_{\pi}$ and $e_{2}\in E_{\pi}$ are _concurrent_ in
$\pi$, denoted by $e_{1}\;||_{\pi}\;e_{2}$, iff $(e_{1},e_{2})\not\in G^{+}$
and $(e_{2},e_{1})\not\in G^{+}$. Intuitively, the fact that event $e_{1}$ is
a cause for event $e_{2}$ means that one has to observe an occurrence of
transition described by $e_{1}$ prior to observing an occurrence of transition
described by $e_{2}$. The fact that two events are concurrent means that the
corresponding transitions can be enabled simultaneously in some occurrence
sequence of the system and be performed one after another in any order. For
process $\pi$ in Figure 5 it holds that $e_{2}\rightarrowtail_{\pi}e_{6}$,
$e_{3}\rightarrowtail_{\pi}e_{4}$, and $e_{5}\;||_{\pi}\;e_{4}$.

The total causal and total concurrent relations are now defined as follows.

###### Definition 4.6 (Total causality and total concurrency).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system and let $x,y\in\mathbb{C}$ be
two non-empty character strings.

  * $\circ$

$x$ and $y$ are _total causal_ in $S$, denoted by
$\mathit{totalCausal}(S,x,y)$, iff
$\forall\,\pi\in\Delta_{S}(x,y)\;\forall\,e_{1}\in E_{\pi}\;\forall\,e_{2}\in
E_{\pi}:(e_{1}\neq
e_{2}\;\land\;\lambda(\rho_{\pi}(e_{1}))=x\;\land\;\lambda(\rho_{\pi}(e_{2}))=y)\Rightarrow
e_{1}\;\rightarrowtail_{\pi}\;e_{2}$.

  * $\circ$

$x$ and $y$ are _total concurrent_ in $S$, denoted by
$\mathit{totalConcurrent}(S,x,y)$, iff
$\forall\,\pi\in\Delta_{S}(x,y)\;\forall\,e_{1}\in E_{\pi}\;\forall\,e_{2}\in
E_{\pi}:(e_{1}\neq
e_{2}\;\land\;\lambda(\rho_{\pi}(e_{1}))=x\;\land\;\lambda(\rho_{\pi}(e_{2}))=y)\Rightarrow
e_{1}\;||_{\pi}\;e_{2}$. $\lrcorner$

For example, $\mathit{totalCausal(S,\texttt{a}^{\prime},\texttt{c})}$ holds
for workflow system $S$ in Figure 4; in every execution of $S$ in which
$\texttt{a}^{\prime}$ and c both occur it holds that every occurrence of
$\texttt{a}^{\prime}$ precedes every occurrence of c. As another example,
$\mathit{totalConcurrent(S,\texttt{c},\texttt{d})}$ holds for the same system.

Predicates over PQL tasks. Next, we lift the PQL predicates from individual
labels to PQL tasks, i.e., to sets of character strings. To this end, we
employ the label unification principle proposed in (Polyvyanyy et al., 2014b).
Given a system $S$ and a character string $x\in\mathbb{C}$, _label
unification_ of $x$ in $S$ is a transformation of $S$ into a fresh system
$S^{\prime}$ that is behaviorally equivalent to $S$ but in which every
occurrence of $x$ is guaranteed to be triggered by a (fresh) dedicated
transition, refer to Definition 6.2 and Lemma 6.5 in (Polyvyanyy et al.,
2014b). Let $X$ be the set of all transitions of $S$ that have label $x$ such
that $|X|>1$. The label unification of $x$ in $S$ augments $S$ to result in a
system $S^{\prime}$ that is behaviorally equivalent to $S$ but ‘forbids’
occurrences of transitions in $X$ and ensures that tokens from the input
places of transitions in $X$ are ‘rerouted’ to the only input place of the
dedicated transition $\hat{t}$ that has label $x$. Note that if $X$ is a
singleton, then all occurrences of $x$ generated by $S$ are guaranteed to be
triggered by transition $t\in X$ and, hence, there is no need to transform
$S$, i.e., it holds that $S^{\prime}=S$.

Figure 6. A system obtained via unification of the set of labels
$\\{\texttt{a},\texttt{a}^{\prime}\\}$ in the workflow system in Figure 4.

The concept of a PQL task is introduced in the language to allow handling
several distinct labels as if they all represent the same activity. For
example, two character strings $\texttt{a}^{\prime}:=$“process payment by
cash” and $\texttt{a}^{\prime\prime}:=$“process payment by check” may be seen
as sufficiently similar to represent activity $\texttt{a}:=$“process payment”.
PQL adapts the label unification principle to operationalize the above
sketched intuition. Figure 6 shows the result of performing label unification
for labels $\texttt{a}^{\prime}$ and $\texttt{a}^{\prime\prime}$ in the system
in Figure 4. The fresh elements introduced during the unification are
highlighted in gray, while the fresh arcs, in addition, are depicted using the
dashed lines. Unlike in the system in Figure 4, transitions with labels
$\texttt{a}^{\prime}$ and $\texttt{a}^{\prime\prime}$ cannot occur in
executions of the system in Figure 6. However, in the transformed system, the
tokens from the input places of the “forbidden” transitions $t_{1}$ and
$t_{2}$ can be rerouted to enable the fresh transition $\hat{t}$ that has
label a and can occur instead of both forbidden transitions; transition
$\hat{t}$ is called the _solitary_ transition for labels $\texttt{a}^{\prime}$
and $\texttt{a}^{\prime\prime}$.

By $\mathit{unify}(S,X)$, $X\in\powerset_{\geq 1}{(\mathbb{C})}$, we denote
the result of the adapted label unification of $X$ in $S$. This result is a
pair $(S^{\prime},\hat{t})$, where $S^{\prime}$ is the transformed system and
$\hat{t}$ is the fresh solitary transition for labels in $X$. For example, it
holds that $\mathit{unify}(S,X)=(S^{\prime},\hat{t})$, where $S$ is the system
in Figure 4, $S^{\prime}$ is the system in Figure 6, and
$X=\\{\texttt{a}^{\prime},\texttt{a}^{\prime\prime}\\}$.

It is easy to see that the order of applying different label unifications has
no impact on the resulting system as long as fresh solitary transitions have
unique labels. Finally, the predicates over PQL tasks are defined as follows.

###### Definition 4.7 (Predicates over PQL tasks).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system and let $X,Y\in\powerset_{\geq
1}{(\mathbb{C})}$ be two non-empty sets of non-empty character strings.

  * $\circ$

$X$ _can occur_ in $S$, denoted by $\mathit{canOccur}(S,X)$, iff
it holds that $\mathit{canOccur}(S^{\prime},x)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$.

  * $\circ$

$X$ _always occurs_ in $S$, denoted by $\mathit{alwaysOccurs}(S,X)$, iff
it holds that $\mathit{alwaysOccurs}(S^{\prime},x)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$.

  * $\circ$

$X$ _can conflict with_ $Y$ in $S$, denoted by $\mathit{canConflict}(S,X,Y)$,
iff it holds that $\mathit{canConflict}(S^{\prime\prime}\\!,x,y)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$ and
$\mathit{unify}(S^{\prime},Y)=(S^{\prime\prime}\\!,y)$.

  * $\circ$

$X$ and $Y$ _can co-occur_ in $S$, denoted by $\mathit{canCooccur}(S,X,Y)$,
iff it holds that $\mathit{canCooccur}(S^{\prime\prime}\\!,x,y)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$ and
$\mathit{unify}(S^{\prime},Y)=(S^{\prime\prime}\\!,y)$.

  * $\circ$

$X$ and $Y$ are in _conflict_ in $S$, denoted by $\mathit{conflict}(S,X,Y)$,
iff
it holds that $\mathit{conflict}(S^{\prime\prime}\\!,x,y)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$ and
$\mathit{unify}(S^{\prime},Y)=(S^{\prime\prime}\\!,y)$.

  * $\circ$

$X$ and $Y$ _co-occur_ in $S$, denoted by $\mathit{cooccur}(S,X,Y)$, iff
it holds that $\mathit{cooccur}(S^{\prime\prime}\\!,x,y)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$ and
$\mathit{unify}(S^{\prime},Y)=(S^{\prime\prime}\\!,y)$.

  * $\circ$

$X$ and $Y$ are _total causal_ in $S$, denoted by
$\mathit{totalCausal}(S,X,Y)$, iff
it holds that $\mathit{totalCausal}(S^{\prime\prime}\\!,x,y)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$ and
$\mathit{unify}(S^{\prime},Y)=(S^{\prime\prime}\\!,y)$.

  * $\circ$

$X$ and $Y$ are _total concurrent_ in $S$, denoted by
$\mathit{totalConcurrent}(S,X,Y)$, iff
it holds that $\mathit{totalConcurrent}(S^{\prime\prime}\\!,x,y)$, where
$\mathit{unify}(S,X)=(S^{\prime},x)$ and
$\mathit{unify}(S^{\prime},Y)=(S^{\prime\prime}\\!,y)$. $\lrcorner$

Using the proposed denotations, one can verify that, for instance,
$\mathit{alwaysOccurs}(S,\\{\texttt{a}^{\prime},\texttt{a}^{\prime\prime}\\})$
evaluates to _true_ , where $S$ is the system in Figure 4. Hence, for example,
one can retrieve the system in Figure 4 by issuing the query “SELECT * FROM *
WHERE AlwaysOccurs($\sim$a);”, given that $\sim$a evaluates to
$\\{\texttt{a}^{\prime},\texttt{a}^{\prime\prime}\\}$. One can use queries
like the one exemplified to perform exploratory querying or address the
problem of the inconsistent usage of labels in process repositories, where
label a from the user specified query gets replaced by labels
$\texttt{a}^{\prime}$ and $\texttt{a}^{\prime\prime}$ from the process
repository.

####  4.6.2. Computations of the PQL Predicates

Definition 4.7 specifies the eight selected predicates over PQL tasks in terms
of the corresponding predicates over transitions. The reader can find
techniques to compute the $\mathit{canConflict}$, $\mathit{canCooccur}$, and
$\mathit{totalCausal}$ predicates over transitions in (Polyvyanyy et al.,
2014b). Using $\mathit{canConflict}$ and $\mathit{canCooccur}$, one can
compute the $\mathit{conflict}$ and $\mathit{cooccur}$ predicates, refer to
Definition 4.7. Next, we propose techniques that given a sound workflow system
$S:=(P,T,F,\lambda,M)$ compute whether $t\in T$ _can occur_ in $S$, $t\in T$
_always occurs_ in $S$, and $t_{1}\in T$ and $t_{2}\in T$ are _total
concurrent_ in $S$. PQL performs these computations on systems obtained via
unifications of sets of labels, refer to Section 4.6.1 and (Polyvyanyy et al.,
2014b) for details. Note that label unification in a sound workflow system
often leads to a system that is not even a workflow system; due to the
introduction of dead transitions, where a dead transition is a transition
which is not part of any occurrence sequence of the system; see for example
transitions $t_{1}$ and $t_{2}$ in Figure 6. Dead transitions are kept in the
resulting systems as they may be required to perform subsequent
transformations. However, once all the transformations are applied, dead
transitions can be removed from the system to result in a sound workflow
system; this trivially follows from the definition of label unification. Note
that in what follows, we restrict some discussions to sound workflow systems.

Can occur transition. One can check whether a transition can occur in a
workflow system by solving a reachability problem on a transformed version of
the system.

###### Definition 4.8 (Can occur transition).

A transition $t\in T$ _can occur_ in a workflow system $S:=(P,T,F,\lambda,M)$
iff there exists an execution $\sigma$ of $S$ such that $t\in\sigma$.
$\lrcorner$

Given a system and marking, the reachability problem consists of deciding if
there is an occurrence sequence of the system that leads to the marking. Note
that the reachability problem is decidable (Hack, 1975).

###### Lemma 4.9 (Can occur transition).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system with a sink place $o\in P$. A
transition $t\in T$ can occur in $S$ iff there exists an occurrence sequence
$\sigma$ of
$S^{\prime}:=(P\cup\\{p^{\prime}\\},T\cup\\{t^{\prime}\\},F\cup\\{(p^{\prime},t^{\prime})\\}\cup\\{(p,t^{\prime})\\!\divides\\!p\in\bullet{t}\\}\cup\\{(t^{\prime},p)\\!\divides\\!p\in{t}\bullet\\},\lambda\cup\\{(t^{\prime},\epsilon)\\},M\cupplus[p^{\prime}])$,
where $p^{\prime}\not\in P$ and $t^{\prime}\not\in T$ are a fresh place and
transition, respectively, such that $t^{\prime}$ is an element of $\sigma$,
i.e., $t^{\prime}\in\sigma$, and $\sigma$ leads to $[o]$. $\lrcorner$

The proof of Lemma 4.9 is straightforward due to the construction of
$S^{\prime}$. If $t$ can occur in $S$, then there exists an execution $\gamma$
of $S$ that contains $t$ at some position $j$ of $\gamma$. A sequence of
transitions obtained from $\gamma$ by replacing $t$ at position $j$ with
$t^{\prime}$ is an occurrence sequence of $S^{\prime}$ that leads to $[o]$.
Let $\sigma$ be an occurrence sequence of $S^{\prime}$ that leads to $[o]$ and
$t^{\prime}\in\sigma$. Then, a sequence of transitions obtained from $\sigma$
by replacing $t^{\prime}$ with $t$ and keeping the order of the remaining
elements is an execution of $S$; note that $\sigma$ contains exactly one
occurrence of $t^{\prime}$.

Always occurs transition. Next, we present a technique for checking whether a
transition always occurs in a sound workflow system.

###### Definition 4.10 (Always occurs transition).

A transition $t\in T$ _always occurs_ in a sound workflow system
$S:=(P,T,F,\lambda,M)$ iff for every execution $\sigma$ of $S$ it holds that
$t\in\sigma$. $\lrcorner$

One can check whether a transition always occurs in a sound workflow system by
solving a reachability problem on a transformed version of the system.

###### Lemma 4.11 (Always occurs transition).

Let $S:=(P,T,F,\lambda,M)$ be a workflow system with a sink place $o\in P$. A
transition $t\in T$ always occurs in $S$ iff there exists no occurrence
sequence $\sigma$ of
$S^{\prime}:=(P\cup\\{p^{\prime}\\},T,F\cup\\{(p^{\prime},t)\\},\lambda,M\cupplus[p^{\prime}])$,
where $p^{\prime}\not\in P$ is a fresh place, that leads to $[p^{\prime},o]$.
$\lrcorner$

The proof of Lemma 4.11 is straightforward due to the construction of
$S^{\prime}$. If $t$ always occurs in $S$, then every execution of $S$
contains $t$. Let $\gamma$ be an execution of $S$ without $t$, then $\gamma$
is an occurrence sequence of $S^{\prime}$ that leads to $[p^{\prime},o]$.
Finally, let $\sigma$ be an occurrence sequence of $S^{\prime}$ that leads to
$[p^{\prime},o]$. Then, clearly, $\sigma$ is an execution of $S$ without $t$.

Total concurrent transitions. Let $S:=(P,T,F,\lambda,M)$ be a workflow system.
By $\Xi_{S}(t_{1},t_{2})$, where $t_{1},t_{2}\in T$, we denote the set
$\\{\pi\in\Pi_{S}\\!\divides\\!\exists\,e_{1},e_{2}\in
E_{\pi}:\rho_{\pi}(e_{1})=t_{1}\;\land\;\rho_{\pi}(e_{2})=t_{2}\\}$.

Figure 7. A workflow system.

###### Definition 4.12 (Total concurrent transitions).

Transitions $t_{1}\in T$ and $t_{2}\in T$ are _total concurrent_ in a sound
workflow system $S:=(P,T,F,\lambda,M)$ iff
$\forall\,\pi\in\Xi_{S}(t_{1},t_{2})\;\forall\,e_{1}\in
E_{\pi}\;\forall\,e_{2}\in E_{\pi}:(e_{1}\neq
e_{2}\;\land\;\rho_{\pi}(e_{1})=t_{1}\;\land\;\rho_{\pi}(e_{2})=t_{2})\Rightarrow
e_{1}\;||_{\pi}\;e_{2}$. $\lrcorner$

The _unfolding_ of a Petri net system is an acyclic graph that encodes all the
processes of the system in a possibly infinite, tree-like structure (McMillan,
1992; Esparza et al., 2002). In (McMillan, 1992), McMillan proposed an
algorithm for constructing a finite initial part of the unfolding, called a
_complete prefix_ of the unfolding, which contains full information about the
behavior of the system, i.e., all the processes of the system.

Figure 7 shows a workflow system $S$ obtained by translating the process model
shown later in Figure 9 (model 9), refer to Section 4.7, into a Petri net
system. Figure 8 shows a complete prefix of the unfolding $U$ of $S$. A
complete prefix of the unfolding of a system $S:=(P,T,F,\lambda,M)$ is a
4-tuple $U:=(B,E,G,\rho)$, where $B$ and $E$ are disjoint sets of conditions
and events, respectively, $G\subseteq(B\times E)\cup(E\times B)$ is the flow
relation, such that $G^{+}$ is irreflexive, and $\rho:B\cup E\rightarrow P\cup
T$ is a function that maps conditions to places and events to transitions.
Thus, a complete prefix of the unfolding is a process that allows forward
conflicts (McMillan, 1992).

Figure 8. A complete prefix of the unfolding of the system in Figure 7.

In Figure 8, conditions and events are shown as circles and rectangles,
respectively. Every condition $b_{i},b^{\prime}_{i},\ldots$ represents one
token at place $p_{i}$, $i\in\mathbb{N}$, refer to (Polyvyanyy et al., 2015b).
Every event $e_{j},e^{\prime}_{j},\ldots$ represents one occurrence of
transition $t_{j}$, $j\in\mathbb{N}$. McMillan proposes to associate every
event $e$ of a compete prefix of the unfolding of a Petri net system with a
marking that one reaches by firing all the transitions encoded by the events
in the local configuration of $e$. The _local configuration_ of an event $e$,
denoted by $\left\lceil e\right\rceil$, is the set of events composed of $e$,
all the events from which there is a directed path to $e$, and no other
events. For example, $\left\lceil
e_{4}\right\rceil=\\{e_{1},e_{2},e_{3},e_{4}\\}$ and $\left\lceil
e_{7}\right\rceil=\\{e_{1},e_{2},e_{3},e_{4},e_{5},e_{6},e_{7}\\}$. One
reaches the marking $[p_{5},p_{6}]$ by firing transitions represented by the
events in $\left\lceil e_{4}\right\rceil$, and the marking $[p_{9}]$ by firing
transitions represented by the events in $\left\lceil e_{7}\right\rceil$.
These markings are encoded by the sets of conditions $\\{b_{5},b_{6}\\}$ and
$\\{b_{9}\\}$ in Figure 8, respectively, and are denoted by
$\mathit{Cut}(\left\lceil e_{4}\right\rceil)$ and $\mathit{Cut}(\left\lceil
e_{7}\right\rceil)$, respectively. Note that the marking $[p_{9}]$ can also be
reached in the system in Figure 7 after occurrences of transitions encoded by
the events in the local configuration of event $e^{\prime}_{7}$.

Intuitively, if one continues constructing the prefix in Figure 8, the part
that will follow $\mathit{Cut}(\left\lceil e^{\prime}_{7}\right\rceil)$ will
be isomorphic to the part of the prefix that will follow
$\mathit{Cut}(\left\lceil e_{7}\right\rceil)$. Hence, McMillan proposed to
stop the construction at $\mathit{Cut}(\left\lceil
e^{\prime}_{7}\right\rceil)$ and refers to $e^{\prime}_{7}$ and $e_{7}$ as a
_cutoff_ and its _corresponding_ event, respectively. We denote the set of all
the cutoff events of a complete prefix of the unfolding $U$ by
$\mathit{cutoffs}(U)$. Given a cutoff event $e$, by $\mathit{corr}(e)$, we
denote the corresponding event of $e$. Thus, $\mathit{cutoffs}(U)$, where $U$
is a complete prefix of the unfolding in Figure 8, is equal to
$\\{e^{\prime}_{7}\\}$, and $\mathit{corr}(e^{\prime}_{7})=e_{7}$. In the
figure, the relation between the cutoff and its corresponding event is shown
by the dotted arrow. For further details on (complete prefixes of) the
unfoldings please refer to (McMillan, 1992; Esparza et al., 2002).

Let $U:=(B,E,G,\rho)$ be a complete prefix of the unfolding of a system
$S:=(P,T,F,\lambda,M)$. Then, it holds that $\mathit{path}(U,e_{1},e_{2})$ iff
$(e_{1},e_{2})\in G^{+}$, or $(e_{2},e_{1})\in G^{+}$, or there exists a
sequence of cutoffs $c\in\mathit{cutoffs}(U)^{*}$ such that (i)
$\exists\,b\in\mathit{Cut}(\left\lceil c_{1}\right\rceil):(e_{1},b)\in G^{+}$,
(ii)
$\exists\,b\in\mathit{Cut}(\left\lceil\mathit{corr}(c_{|c|})\right\rceil):(b,e_{2})\in
G^{+}$, and (iii)
$\forall\,i\in[1..(|c|-1)]\exists\,b_{1}\in\mathit{Cut}(\left\lceil\mathit{corr}(c_{i})\right\rceil)\exists\,b_{2}\in\mathit{Cut}(\left\lceil
c_{i+1}\right\rceil):(b_{1},b_{2})\in G^{*}$.

###### Lemma 4.13 (Total concurrent transitions).

Let $S:=(P,T,F,\lambda,M)$ be a sound workflow system and let
$U:=(B,E,G,\rho)$ be a complete prefix of the unfolding of $S$. Transitions
$t_{1}\in T$ and $t_{2}\in T$ are total concurrent in $S$ iff $\forall
e_{1}\\!\in E\,\forall e_{2}\\!\in E:(e_{1}\neq
e_{2}\;\land\;\rho(e_{1})=t_{1}\;\land\;\rho(e_{2})=t_{2})\Rightarrow\neg\;\mathit{path}(U,e_{1},e_{2})$.
$\lrcorner$

Let us assume that $t_{1}$ and $t_{2}$ are total concurrent in $S$ and there
exist two distinct events $e_{1}$ and $e_{2}$ that describe occurrences of
$t_{1}$ and $t_{2}$, respectively, such that $\mathit{path}(U,e_{1},e_{2})$.
Then, there is a process in $\Xi_{S}(t_{1},t_{2})$ that contains two distinct
causal events that refer to $t_{1}$ and $t_{2}$. This follows immediately from
the definition of a complete prefix of the unfolding, cf. (Esparza et al.,
2002), and the fact that every occurrence sequence of $S$ can be extended to
an execution. If for every two distinct events $e_{1}$ and $e_{2}$ that
describe occurrences of $t_{1}$ and $t_{2}$ it holds that
$\neg\,\mathit{path}(U,e_{1},e_{2})$, then $t_{1}$ and $t_{2}$ are total
concurrent in $S$, as according to the definition of a complete prefix of the
unfolding there exists no process in $\Xi_{S}(t_{1},t_{2})$ that evidences
that some occurrences of $t_{1}$ and $t_{2}$ are causal.

Note that one can always construct a complete prefix of the unfolding of a
bounded system (Esparza et al., 2002), i.e., a system with a finite number of
reachable states, while a sound workflow system is guaranteed to be bounded
(van der Aalst, 1997). Using the prefix in Figure 8 and Lemma 4.13 one can
verify whether two given transitions are total concurrent in the system $S$ in
Figure 7. For example, transitions $t_{3}$ and $t_{5}$ are total concurrent in
$S$. Transitions $t_{3}$ and $t_{6}$ are not total concurrent in $S$ because
of events $e_{3}$ and $e^{\prime}_{6}$ and the fact that
$(e_{3},e^{\prime}_{6})\in G^{+}$. Transitions $t_{9}$ and $t_{11}$ are also
not total concurrent in $S$ because of events $e_{9}$ and $e_{11}$ and the
sequence of cutoff events $\left\langle e^{\prime}_{7}\right\rangle$; note
that $(e_{9},b^{\prime}_{9})\in G^{+}$ and $(b_{9},e_{11})\in G^{+}$.

###  4.7. Sample PQL Queries

We now consider an example process repository consisting of ten process models
that are sourced from the collection of the SAP R/3 reference model (Curran et
al., 1998) as well as from Polyvyanyy’s PhD thesis (Polyvyanyy, 2012). Figure
9 depicts the ten process models using BPMN. In a BPMN model, activities are
used to model tasks and are drawn as rectangles. Gateways are visualized as
diamonds. Exclusive gateways use a marker which is shaped like “$\times$”
inside the diamond shape, wheres parallel gateways use a marker which is
shaped like “$+$” inside the diamond shape. Directed arcs encode control flow
dependencies. For simplicity, the models in Figure 9 use only abstract task
labels (which are alphabet letters). In addition, the attributes information
of each process model, including its ID, version, date created, and author, is
shown in the text annotation under the model.

The example process model repository discussed in this section can be
formalized as the 6-tuple $(S,A,L,\mathit{val},\mathit{loc},\precsim)$, refer
to Definition 4.1, where $S$ is the set of ten Petri net systems
$\\{s_{1},\ldots,s_{10}\\}$, $s_{i}$, $i\in\\{1..10\\}$, captures the behavior
of model $i$ in Figure 9; the corresponding net systems can be obtained from
BPMN models using the approach from (Dijkman et al., 2008), $A:=$ {ID,
Version, Date, Author} is the set of attribute names,
$L:=\\{/,\,\,/\texttt{Ten-Models-BPMN},\,\,/\texttt{SAP-R3-EPC-Repo}\\}$ is
the set of locations, $\mathit{val}:=$ {($s_{1}$, ID, 1), ($s_{1}$, Version,
1.0), ($s_{1}$, Date, 01-June-2017), $\ldots$} is the attribute value
assignment function, $\mathit{loc}:=\cup_{i\in\\{1..10\\}}(s_{i},/\texttt{Ten-
Models-BPMN})$ is the location assignment function, and $\precsim$ is the
location map such that $(l,l)\in\,\,\precsim$ for every $l\in L$, and
$(/\texttt{Ten-Models-BPMN},/)\in\,\,\precsim$ and $(/\texttt{SAP-R3-EPC-
Repo},/)\in\,\,\precsim$.

Figure 9. A repository of ten process models (in BPMN) with their attributes
information and results of evaluation of ten sample queries over each of these
models.

The process models in Figure 9 have various structural features and are sound.
The first five models (models 1 to 5) capture acyclic processes and the other
five (models 6 to 10) specify processes that contain cycles. Models 1, 2, 6,
and 10 are well-structured, where a process model is _well-structured_ if and
only if every node with multiple outgoing arcs (a split) has a corresponding
node with multiple incoming arcs (a join), and vice versa, such that the set
of nodes between the split and the join induces a SESE component (Polyvyanyy
et al., 2010); otherwise the model is said to be _unstructured_ (Polyvyanyy,
2012). Models 3, 4, 5, 7, 8, and 9 in Figure 9 are unstructured. Model 7, 8,
and 9 can be mapped to well-structured models. For example, model 10 is
equivalent to model 9 and is well-structured. Note that models 3 to 5 are
inherently unstructured, i.e., the behaviors they describe do not have
equivalent well-structured representations (if the concurrency relations
between process tasks must be preserved) (Polyvyanyy, 2012). Among these
models, model 4 has a typical Z-structure (Kiepuszewski et al., 2000), which
is formed by the control flow dependencies between tasks $A$, $B$, $C$, and
$D$.

Next, we propose ten sample queries:

  * Q1.

SELECT "Author" FROM "/Ten-Models-BPMN"

  * WHERE CanOccur("D") AND Conflict("D","E");

  * Q2.

SELECT "Version" FROM "/Ten-Models-BPMN"

  * WHERE AlwaysOccurs("C") OR Cooccur("B","C");

  * Q3.

SELECT "Date" FROM "/Ten-Models-BPMN"

  * WHERE (CanOccur("G") AND (NOT Conflict("E","G"))) OR

  * (TotalConcurrent("C","D") AND AlwaysOccurs("D"));

  * Q4.

SELECT "Author","Version" FROM "/Ten-Models-BPMN"

  * WHERE CanOccur({"F","G"},ALL) AND AlwaysOccurs({"F","G"},ANY);

  * Q5.

SELECT "Version","Date" FROM "/Ten-Models-BPMN"

  * WHERE Cooccur("B",{"C","D"},ALL) AND TotalConcurrent("B",{"C","D"},ANY);

  * Q6.

SELECT "Version","Author" FROM "/Ten-Models-BPMN"

  * WHERE Conflict({"A","B"},{"E","F"},ANY) OR

  * (Cooccur({"A","B"},{"E","F"},EACH) AND

  * TotalCausal({"A","B"},{"E","F"},ALL));

  * Q7.

SELECT "Date","Author" FROM "/Ten-Models-BPMN"

  * WHERE "C" IN (GetTasksAlwaysOccurs({"C"}) UNION

  * GetTasksTotalCausal({"C"},{"B","D"},ALL));

  * Q8.

SELECT "Date","Version" FROM "/Ten-Models-BPMN"

  * WHERE "G" IN (GetTasksCanOccur({"G"}) INTERSECT

  * GetTasksConflict({"G"},{"D","E","F"},ANY));

  * Q9.

SELECT "Version","Date","Author" FROM "/Ten-Models-BPMN"

  * WHERE GetTasksCooccur({"A","B","C"},{"D","E"},ANY) NOT EQUALS

  * GetTasksTotalConcurrent({"A","B","C"},{"D","E"},ANY);

  * Q10.

SELECT * FROM "/Ten-Models-BPMN" WHERE ({"A","B","E","F"} EXCEPT

  * GetTasksCooccur({"A","B","E","F"},{"C","D"},ALL)) OVERLAPS WITH

  * GetTasksConflict({"A","B","E","F"},{"C","D"},ANY);

The PQL constructs used to specify these queries include the atomic behavioral
predicates, the corresponding predicate macros, logical operations (over
predicates and predicate macros), construction of task sets using predicates,
set operations, and set comparison operations. Note that these sample queries
(named Q1–Q10), are instantiations of ten query templates (out of a total of
150 query templates listed in Appendix C) to be used for evaluation of PQL in
Section 6.1.

We executed the above ten queries on the repository of ten process models
shown in Figure 9. Each query was evaluated over each of these ten process
models according to the semantics of PQL (defined in Sections 4.5 and 4.6).
The evaluation result indicates whether a process model satisfies the
condition specified in the WHERE clause of a specific query. In Figure 9, this
is depicted by a query name being ticked or not ticked under each process
model. Note that since models 9 and 10 are behaviorally equivalent, every
query evaluation over these models yields the same result.

Table 6. Answers to ten sample queries over the repository of ten process models in Figure 9. Query | Query result
---|---
Q1 |  {($s_{1}$,{(Author, SAP)}), ($s_{5}$,{(Author, Polyvyanyy)})}
Q2 |  {($s_{1}$,{(Version, 1.0)}), ($s_{4}$,{(Version, 1.2)}), ($s_{6}$,{(Version, 2.0)}), ($s_{7}$,{(Version, 1.2)}),
|  ($s_{9}$,{(Version, 1.2)}), ($s_{10}$,{(Version, 2.0)})}
Q3 |  {($s_{4}$,{(Date, 31-May-2017)}), ($s_{6}$, {(Date, 01-June-2017)}), ($s_{7}$,{(Date, 01-June-2017)}),
|  ($s_{9}$,{(Date, 05-June-2017)}), ($s_{10}$,{(Date, 05-June-2017)})}
Q4 |  {($s_{6}$,{(Author, SAP), (Version, 2.0)}), ($s_{9}$,{(Author, Polyvyanyy), (Version, 1.2)}),
|  ($s_{10}$,{(Author, Polyvyanyy), (Version, 2.0)})}
Q5 |  {($s_{4}$,{(Version, 1.2), (Date, 31-May-2017)}), ($s_{9}$,{(Version, 1.2), (Date, 05-June-2017)}),
|  ($s_{10}$,{(Version, 2.0), (Date, 05-June-2017)})}
Q6 |  {($s_{1}$,{(Version, 1.0), (Author, SAP)}), ($s_{2}$,{(Version, 1.1), (Author, SAP)}),
|  ($s_{3}$,{(Version, 2.0), (Author, Polyvyanyy)})}
Q7 |  {($s_{1}$,{(Date, 01-June-2017), (Author, SAP)}), ($s_{2}$,{(Date, 31-May-2017), (Author, SAP)}),
|  ($s_{3}$,{(Date, 03-June-2017), (Author, Polyvyanyy)}), ($s_{4}$,{(Date,
31-May-2017), (Author, SAP)}),
|  ($s_{7}$,{(Date, 01-June-2017), (Author, SAP)}), ($s_{9}$,{(Date,
05-June-2017), (Author, Polyvyanyy)}),
|  ($s_{10}$,{(Date, 05-June-2017), (Author, Polyvyanyy)})}
Q8 |  {($s_{8}$, {(Date, 03-June-2017), (Version, 2.0)})}
Q9 |  {($s_{3}$,{(Version, 2.0), (Date, 03-June-2017), (Author, Polyvyanyy)}), ($s_{4}$,{(Version, 1.2),
|  (Date, 31-May-2017), (Author, SAP)}), ($s_{5}$,{(Version, 1.2), (Date,
03-June-2017),
|  (Author, Polyvyanyy)}), ($s_{6}$,{(Version, 2.0), (Date, 01-June-2017),
(Author, SAP)}),
|  ($s_{7}$,{(Version, 1.2), (Date, 01-June-2017), (Author, SAP)}),
($s_{9}$,{(Version, 1.2),
|  (Date, 05-June-2017), (Author, Polyvyanyy)}), ($s_{10}$,{(Version, 2.0),
| (Date, 05-June-2017), (Author, Polyvyanyy)})}
Q10 |  {($s_{1}$,{(ID, 1), (Version, 1.0), (Date, 01-June-2017), (Author, SAP)}), ($s_{2}$,{(ID, 2), (Version, 1.1),
|  (Date, 31-May-2017), (Author, SAP)}), ($s_{3}$,{(ID, 3), (Version, 2.0),
(Date, 03-June-2017),
|  (Author, Polyvyanyy)}), ($s_{5}$,{(ID, 5), (Version, 1.2), (Date,
03-June-2017), (Author, Polyvyanyy)}),
|  ($s_{6}$,{(ID, 6), (Version, 2.0), (Date, 01-June-2017), (Author, SAP)})}

Table 6 summarizes the results of executing the ten sample queries. For each
query, only the corresponding systems (and their attributes) that satisfy the
WHERE condition of the query are retrieved. For example, Query Q1 is designed
to retrieve those process models where (i) task labeled "D" (task D for short)
occurs in at least one process instance (CanOccur("D")) and (ii) there is no
process instance in which tasks D and E both occur (Conflict("D","E")). The
first condition holds in all models in Figure 9, while the second condition
holds in models 1 and 5 only. It is important to understand the behavior of a
process model when evaluating the second condition. For example, in model 8,
although tasks D and E are on two exclusive branches (subsequent to task B),
both tasks may occur in one process instance since task D is part of a cycle.
Another interesting example concerns query Q3, in particular, the condition
TotalConcurrent("C","D") in the query. This condition holds for a process
model if and only if for every instance in which tasks C and D both occur
every occurrence of task C can be executed at the same time with every
occurrence of task D. For example, due to the characteristics of model 3,
i.e., it is unstructured, it is hard to evaluate this condition without
knowledge of the model’s behavior.

##  5\. Implementation

The proposed in the previous section querying method has been implemented and
is publicly available.141414https://github.com/processquerying/PQL.git The
implementation exhibits a well-defined application programming interface (API)
to facilitate its integration with other software products. This API can be
accessed by the users via command-line interfaces (CLIs) of two utilities: the
PQL bot and the PQL tool. We refer to them as _PQL Tools_ and, conjointly,
they implement the _PQL environment_. The PQL bot is used to prepare models
for querying, while the PQL tool is used to execute PQL queries over the
indexed models.

The PQL environment is implemented using Java, ANTLR, and MySQL technologies.
The Java language is chosen due to its “architecture-neutral and portable”
principle. As a result, the environment can be deployed on various platforms
running different operating systems. The PQL tool uses an ANTLR (Parr, 2013)
generated parser that can build and walk syntax trees of PQL queries. Given a
context-free grammar expressed using extended Backus-Naur Form (Hopcroft et
al., 2006) as input, ANTLR automatically generates Java code of a parser of
the grammar. The PQL grammar, which incorporates both the abstract and
concrete syntax proposed in Section 4.3 and Section 4.4, respectively,
captured using ANTLR notation is listed in Appendix B. To improve execution
times of PQL queries, the PQL tool relies on an index of behavioral
relations—a special data structure that improves the computation speed of
behavioral relations at the cost of time for its construction and space for
its storage. The tool uses this index at runtime to avoid having to freshly
compute PQL predicates every time a new query is issued. The index is stored
in a MySQL relational database system.

The two PQL utilities load their configuration parameters from the global
initialization file. These parameters set values to configure database
connections, a path to a model checker used by PQL bots, configuration
parameters of an information retrieval engine for assessment of label
similarities, the default and indexed label similarity thresholds, the maximum
number of threads used by the PQL tool when executing queries, the time that
PQL bots sleep (i.e., stay idle) between two subsequent indexing jobs, and the
maximal allowed time to index a single model. It is easy to configure the PQL
environment to use any third-party tool for scoring label similarities, to
fulfill the process querying requirements. At the moment, one can configure
the PQL environment to use one of the three integrated information retrieval
engines to be used when scoring label similarities. These are Apache
Lucene151515https://lucene.apache.org/, Themis-IR (Polyvyanyy, 2007), and an
implementation of the label similarity scoring approach based on the
Levenshtein distance. The Apache Lucene and Themis-IR engines are configured
to use the vector space model to perform label similarity assessments, while
the approach based on the Levenshtein distance is implemented based on the
principles proposed in (Li and Liu, 2007).

The PQL bot and the PQL tool are discussed in Section 5.1 and Section 5.2,
respectively. Section 5.3 is devoted to the discussion of the integration of
the PQL environment with Apromore—an open source process model repository (La
Rosa et al., 2011).

###  5.1. The PQL Bot

The PQL bot is a standalone utility that can be used to systematically index
models stored by the PQL tool. Once a model is indexed, it can be matched to a
query. One can start multiple PQL bot instances simultaneously to index
multiple models in parallel. To construct an index, a PQL bot instance
computes all the behavioral predicates over all the PQL tasks of the model and
stores them in the database. A call to the PQL indexing routine takes a
workflow system described in the Petri Net Markup Language (PNML) format as
input. The PNML format is an XML-based syntax for high-level Petri nets, which
has been designed as a standard interchange format aimed at enabling Petri net
tools to exchange Petri net models (Billington et al., 2003). For many high-
level process modeling languages, such as WS-BPEL, EPC, and BPMN, there exist
mappings to the Petri net formalism. As a result, the PQL environment can work
with models developed using a wide range of modeling tools captured using many
mainstream notations. For more information on Petri nets and workflow systems
refer to Section 3.2. This section also summarizes the technique for
translating process models into workflow systems that was used in the reported
implementation of the PQL bot; it is the technique for converting the EPC in
Figure LABEL:fig:EPC into the workflow system in Figure LABEL:fig:system.

When initializing a PQL bot instance one can configure it via CLI. Some
options of the PQL bot CLI are listed in Table 7. Every PQL bot instance has a
unique name, which can be assigned using option -n. If this option is not
used, a random unique name is assigned. Once started, a PQL bot instance
indexes stored (but not yet indexed) models in succession. One can use CLI
options -s and -i to specify time to sleep, i.e., to stay idle, between two
successive indexing tasks, and the maximal time to attempt indexing of a
model. If these options are not used, the parameters get configured based on
the values in the global configuration file. If indexing of a model could not
be completed within the given time frame, the model is marked as such that can
not be indexed using this version of the bot, and the bot proceeds with
indexing the next model. The -h and -v CLI options, respectively, print the
help message and get the version of the invoked PQL bot instance.

Table 7. CLI options of the PQL bot. Option | Option (short) | Parameter | Description
---|---|---|---
\--help | -h |  | Print help message
\--index | -i | <number> | Maximal indexing time (in seconds)
\--name | -n | <string> | Name of this bot (maximum 36 characters)
\--sleep | -s | <number> | Time to sleep between indexing jobs (in seconds)
\--version | -v |  | Get version of this bot

Once started, a PQL bot instance run as a daemon, i.e., a background process,
until it is shut down. An example of the command line output of a PQL bot
instance is listed below.

>> java -jar PQL.BOT-1.0.jar -n=Brisbane -s=60 -i=86400
>> =======================================================================
>> Process Query Language (PQL) Bot ver. 1.0
>> =======================================================================
>> Name: Brisbane
>> Sleep time: 60s
>> Max. index time: 86400s
>> =======================================================================
>> 10:45:18.487 Brisbane - There are no pending jobs
>> 10:45:18.487 Brisbane - Sent an alive message
>> 10:45:18.497 Brisbane - Going to sleep for 60 seconds
>> 10:46:18.505 Brisbane - Woke up
>> 10:46:18.525 Brisbane - Retrieved indexing job for the model with ID 1
>> 10:46:18.575 Brisbane - Start checking model with ID 1
>> 10:46:23.506 Brisbane - Finished checking model with ID 1
>> 10:46:23.506 Brisbane - Start indexing model with ID 1
>> 10:47:03.608 Brisbane - Finished indexing model with ID 1
>> 10:47:03.608 Brisbane - Going to sleep for 60 seconds
>> 10:48:03.613 Brisbane - Woke up
>> 10:48:03.623 Brisbane - Retrieved indexing job for the model with ID 2
>> 10:48:03.673 Brisbane - Start checking model with ID 2
>> 10:48:13.248 Brisbane - Finished checking model with ID 2
>> 10:48:13.249 Brisbane - Start indexing model with ID 2
>> 10:49:52.679 Brisbane - Finished indexing model with ID 2
>> 10:49:52.679 Brisbane - Going to sleep for 60 seconds
>> 10:50:52.704 Brisbane - Woke up
>> 10:50:52.704 Brisbane - There are no pending jobs
>> ...

The computation of a PQL predicate reduces to one of these three problems: the
_reachability problem_ (Hack, 1975), the _covering problem_ (Rackoff, 1978),
or the _structural analysis over a complete prefix_ (McMillan, 1992; Esparza
et al., 2002) of the _unfolding_ (Nielsen et al., 1981) of the system; refer
to Section 4.6 and (Polyvyanyy et al., 2014b). The PQL bot uses the solutions
to the reachability and covering problems implemented in the LoLA tool version
2.0 (Schmidt, 2000).161616http://service-technology.org/lola/ LoLA uses state-
of-the-art state space reduction techniques to check whether a Petri net
system satisfies a given property. When constructing finite complete prefixes
of unfoldings, the PQL bot reuses the implementation of the algorithm from
(Esparza et al., 2002) available as part of the jBPT initiative (Polyvyanyy
and Weidlich, 2013).

###  5.2. The PQL Tool

The PQL tool can be used to store, index, delete, and query process models.
Table 8 lists some CLI options of the PQL tool. For example, the PQL tool
allows a user to store a given model (option -s), check if a model can be
indexed (option -c), index a model (option -i), delete a model and its index
(option -d), visualize the parse tree of a given query (option -p), execute a
query (options -q), and reset the PQL environment (option -r). The CLI can be
used to access help information (option -h) and the version of the tool
(option -v).

Table 8. CLI options of the PQL tool. Option | Option (short) | Parameter | Description | Requires option
---|---|---|---|---
\--check | -c |  | Check if model can be indexed | -id
\--delete | -d |  | Delete model (and its index) | -id
\--help | -h |  | Print help message |
\--index | -i |  | Index model | -id
\--identifier | -id | <string> | Model identifier | -id
\--parse | -p |  | Show PQL query parse tree | -pql
\--pnmlPath | -pnml | <path> | PNML path |
\--pqlPath | -pql | <path> | PQL path |
\--query | -q |  | Execute PQL query | -pql
\--reset | -r |  | Reset this PQL instance |
\--store | -s |  | Store model |  -pnml (-id)
\--version | -v |  | Get version of this tool |

To store models, the CLI option -s must be accompanied by option -pnml that
specifies a path either to a single PNML file or to a directory that contains
PNML files. If a path to a PNML file is used, the call to the PQL tool must
include option -id to specify a unique identifier to associate with the model.
Otherwise, models are attempted to be stored using their file names as unique
identifiers. Once stored, a model can be indexed by a PQL bot instance or by
the PQL tool using the CLI option -i accompanied by option -id that specifies
the unique identifier that was used to store the model. When indexing a model,
the PQL tool uses the same routines as the PQL bot.

Note that the dynamic semantics of PQL is implemented over sound workflow
systems—a special class of Petri net systems, refer to Section 4.6 for
details. One can check whether a given Petri net system is a sound workflow
system by calling the PQL tool with option -c. Note that every request to
index a model in the PQL environment is automatically preceded by a soundness
check of this model. Alternatively, a user may delete a model using option -d.
By deleting a model, the user also deletes its index. Both options -c and -d
require option -id to uniquely identify a model to be checked and deleted,
respectively. To execute a PQL query, a user can use option -q together with
option -pql that specifies a path to a file that contains a PQL query captured
using the concrete syntax proposed in Section 4.4. To visualize the parse tree
of a PQL query, one can use option -p together with option -pql. Finally, one
can reset the PQL environment using option -r. By resetting the environment,
one deletes all stored models and indexes.

An example command line output of executing a PQL query that is discussed in
detail in Section 4.6 using the PQL tool is shown below.

>> java -jar PQL.TOOL-1.0.jar -q -pql=query.pql
>> PQL query: SELECT * FROM * WHERE AlwaysOccurs("process payment"[0.75]);
>> Attributes: [UNIVERSE]
>> Locations: [UNIVERSE]
>> Task: "process payment"[0.75] -> ["process payment by cash","process
payment by check"]
>> Result: [Fig.4.pnml]

The PQL tool supports multi-threaded querying. A user can configure the number
of query threads to be used when evaluating queries in the global
configuration file. As a result of executing a PQL query, the tool returns a
collection of matching models and PQL tasks (sets of activity labels) that
were used to retrieve the models.

###  5.3. Integration with Apromore

PQL tools have been integrated with Apromore—an open source process model
repository (La Rosa et al., 2011), refer to (Polyvyanyy et al., 2015a) for
details. Apromore can store models developed using many of the commonly used
notations. It allows users to edit and analyze the stored models.

Figure 10. The PQL query editor in Apromore.

Process models in the Apromore repository get converted to Petri net systems
and then indexed by the PQL bots. The interface of Apromore has been extended
to allow users to specify PQL queries. The interface is designed to improve
user experience, for example, by suggesting standard PQL keywords and allowing
to drag-and-drop process models to be considered as part of the FROM clause. A
PQL query entered using the Apromore interface is passed to the PQL tool.
Based on the constructed indexes, the PQL tool evaluates the query. The result
of the query, i.e., a set of the unique identifiers of models that match the
query, is channeled back to Apromore. Apromore then displays to the user the
list of models (and their attributes) that match the query. The user can
examine the matching models using the Apromore’s model editor.

The reader can take a look at a screencast that demonstrates the use of PQL in
Apromore, cf. https://www.youtube.com/watch?v=S_U6frTWd3M. Figure 10 shows a
screenshot of the Apromore’s PQL query editor. The editor specifies a query
similar to query Q10 from Section 4.7. In contrast to query Q10, the query in
Figure 10 uses two variables ‘x’ and ‘y’, and requests to be executed over the
latest versions of two models with names ‘4’ and ‘10’ located in folder
‘Home/pql/’.

Figure 11 shows another screenshot with information on the execution of yet
another PQL query. Concretely, the information displayed is the explanation of
the label similarities used to execute the query. As label “compensation plan
is approved” is an instance of the ExactTask construct, according to the
semantics of PQL, it resolves into the singleton that contains the label. Note
that label “delegation of requirement for planning” is an instance of the
DefSimTask construct. The PQL Tool used to execute this query was configured
to use the default label similarity threshold of 0.75. Based on the configured
engine for scoring label similarities, and the threshold, the PQL tool has
discovered three similar labels shown in the figure.

Figure 11. The PQL query info window, borrowed from (Polyvyanyy et al.,
2015a).

##  6\. Evaluation

Using the implementation from Section 5, we conducted a series of experiments
to assess the performance of PQL in terms of indexing and querying time. The
experiments were performed on a computer with 8GB of RAM and 3.4GHz quad-core
Intel Core CPU (8 logical processors), running Windows 7 and JVM 1.7. The
results demonstrate the feasibility and scalability of using PQL in industrial
settings. Section 6.1 proceeds with a presentation of the datasets used in the
evaluation.

###  6.1. Datasets

Process models. The study was conducted using 493 industrial and 1,000
synthetic process models.171717The synthetic models are available at:
https://www.dropbox.com/s/plrlqe1ewsxwy3b/pnml-1000.zip?dl=0. All the 1,493
models are sound workflow systems; the reader can refer to Section 3 for more
information on sound workflow systems. We obtained the industrial models from
the SAP R/3 Reference Model (Curran et al., 1998), which is a collection of
604 EPCs in various domains such as sales, production, and procurement used to
customize the SAP R/3 ERP system. We converted the EPCs to Petri net systems
and then completed them to workflow systems. Next, we filtered out the unsound
systems, resulting in 493 sound models. We complemented this collection of
real-life models with a collection of synthetic workflow systems, which we
generated using the tool described in (Yan et al., 2015). This tool takes a
seed process model collection and generates models that share similar
structural and label characteristics to the seed. We used the 604 EPCs in the
SAP R/3 collection as a seed, with a multiplier of 50, to generate 30,200
artificial EPCs. We converted these EPCs into workflow systems and filtered
out the unsound models, leading to 16,769 sound workflow systems. Finally,
from these 16,769 systems, we randomly selected 1,000 systems, each with more
than 10 nodes.

Table 9. Structural characteristics of the industrial process models. | #P | #T | #F | #OT | #XS | #XJ | #AS | #AJ | #PG | #B | #R
---|---|---|---|---|---|---|---|---|---|---|---
Average | 17.85 | 15.91 | 35.7 | 8.57 | 0.64 | 0.65 | 1.13 | 1.13 | 5.73 | 1.78 | 0.002
Minimum | 4 | 3 | 6 | 2 | 0 | 0 | 0 | 0 | 1 | 0 | 0
Maximum | 74 | 86 | 180 | 35 | 6 | 6 | 6 | 6 | 31 | 9 | 1
Std. Dev. | 12.73 | 11.89 | 27.61 | 6.21 | 0.89 | 0.91 | 1.21 | 1.22 | 4.93 | 1.66 | 0.05

Tables 9 and 10 provide statistics on the structural properties of the two
model collections. The tables list basic statistics on the number of places
(#P), transitions (#T), flow arcs (#F), observable transitions (#OT), XOR-
splits (#XS), XOR-joins (#XJ), AND-splits (#AS), AND-joins (#AJ), polygons
(#PG), bonds (#B), and rigids (#R) in the models of both collections, which
are the metrics for comparing the structural properties of model collections
employed in (Yan et al., 2015). By XOR-join and XOR-split we refer to a place
with multiple input transitions and a place with multiple output transitions,
respectively. By AND-join and AND-split we refer to a transition with multiple
input places and a transition with multiple output places, respectively.
Polygons, bonds and rigids are different types of SESE components in the WF-
tree of a workflow system (Weidlich et al., 2011), where a polygon is a
sequence of SESE components in which every two subsequent components share one
node, a bond is a collection of SESE components that share entry and exit
nodes, and a rigid is an unstructured component (Polyvyanyy, 2012). The tables
demonstrate that industrial and synthetic models have similar structural
characteristics.

Table 10. Structural characteristics of the synthetic process models. | #P | #T | #F | #OT | #XS | #XJ | #AS | #AJ | #PG | #B | #R
---|---|---|---|---|---|---|---|---|---|---|---
Average | 16.63 | 13.52 | 32.4 | 10.95 | 0.45 | 0.43 | 1.26 | 1.22 | 6.192 | 1.609 | 0.116
Minimum | 5 | 5 | 10 | 3 | 0 | 0 | 0 | 0 | 1 | 0 | 0
Maximum | 86 | 84 | 190 | 67 | 8 | 5 | 7 | 6 | 39 | 8 | 2
Std. Dev. | 11.14 | 9.01 | 23.08 | 7.48 | 0.85 | 0.77 | 1.04 | 0.98 | 4.99 | 1.15 | 0.34

Queries. We designed 150 PQL query templates. Each template is a PQL query
with placeholders for activity labels. During the experiments, the
placeholders were instantiated with random labels. The query templates were
developed to exploit the various features of the PQL grammar. According to the
PQL features they support, these query templates were divided into three
categories and further subdivided into groups and subgroups. Table 11 lists
all the PQL query categories, groups, and subgroups, and provides numbers of
query templates accordingly (see column “# Templates”). All the PQL query
templates used in the experiments are listed in Appendix C.

Table 11. Categories, Groups, and Subgroups of PQL query templates. Category.Group.Subgroup | Name | # Templates
---|---|---
1.a | Unary atomic predicates | 2
1.b | Binary atomic predicates | 4
2.a.1 | Negations of predicates (Same) | 6
2.a.2 | Conjunctions of predicates (Same) | 18
2.a.3 | Disjunctions of predicates (Same) | 18
2.b.1 | Conjunctions of predicates (Mixed) | 3
2.b.2 | Disjunctions of predicates (Mixed) | 3
2.b.3 | Combinations of logical operations | 2
3.a.1 | Unary predicate macros | 12
3.a.2 | Binary predicate macros (Task-Set) | 24
3.a.3 | Binary predicate macros (Set-Set) | 36
3.b.1 | Constructions via unary predicates | 2
3.b.2 | Constructions via binary predicates | 8
3.b.3 | Constructions with set operations | 5
3.b.4 | Constructions with set comparisons | 7

The first category contains six query templates capturing individual atomic
behavioral predicates. These can be divided into two groups, one covering the
two unary predicates (1.a), the other covering the four binary predicates
(1.b).

The second category is a result of combining atomic predicates via logical
operations. There are two groups, one for connecting the same predicates
(2.a), the other for connecting mixed predicates (2.b). The former group can
be further divided into three subgroups which capture, respectively, the
negation of each predicate (2.a.1), the conjunctions of each predicate twice,
three, or four times (2.a.2), and the disjunctions of each predicate twice,
three, or four times (2.a.3). The latter group also has three subgroups which
capture, respectively, the conjunctions of any two, three, or four different
predicates (2.b.1), the disjunctions of any two, three, or four different
predicates (2.b.2), and a couple of different combinations of three logical
operations between mixed predicates (2.b.3).

The third category captures predicate macros in one group (3.a) and
construction of task sets using predicates in the other group (3.b). The first
group has three subgroups. One applies each of the unary predicate macros over
a task set of two, three, or four tasks in conjunction (ALL) or in disjunction
(ANY) (3.a.1); one applies each of the binary predicate macros between a
single task and a task set of two, three, or four tasks in conjunction or in
disjunction (3.a.2); and one applies each of the binary predicate macros
between two task sets each consisting of two, three, or four tasks (3.a.3).
The second group has four subgroups. The first two subgroups apply the set
predicate TaskInSetOfTasks to a task set that is constructed using unary
behavioral predicates (3.b.1) or using binary predicates (3.b.2). The last two
subgroups capture task set constructions using mixed behavioral predicates
with set operations (3.b.3) or set comparisons (3.b.4).

###  6.2. Indexing Performance

We conducted four experiments to measure the performance of PQL bots and the
impact of different factors on indexing time. In what follows, for each of
these four experiments, we detail its setup and discuss the obtained
measurements.

Experiment 1.1: Impact of PQL bots on indexing time. The goal of this
experiment was to measure the performance of PQL bots. We measured the time of
indexing the industrial and synthetic models using different numbers of bots
(from 1 to 8). Each indexing exercise was repeated three times and we recorded
the average indexing times of the three runs. In all the runs, the bots were
configured to only index the label similarity threshold of 1.0. The procedure
was repeated for different parts of the process model collections, i.e., using
25%, 50%, 75% and 100% of models in each collection. Models for each part of
each process model collection were selected randomly.

Figure 12. Impact of PQL bots on indexing time: (a) industrial models and (b)
synthetic models.

Figure 12 plots the indexing times (in seconds) for different parts of process
model collections against different numbers of PQL bots for (a) the industrial
models and (b) the synthetic models. The two plots demonstrate that adding
bots decreases indexing time, though the decrease in indexing time gets less
pronounced with the increase of the number of bots. Indexing of the whole
collection of industrial models with one bot took 6 hours and 54 minutes. Two
bots managed to index 493 systems in 3 hours and 28 minutes (approximately two
times faster than with one bot). Note that eight bots spent 1 hour and 12
minutes indexing the same collection (5.8 times faster than with one bot). A
similar trend can be observed for the synthetic models. The relationship
between the indexing time and the number of bots is best described by the
power function $y=t\times x^{k}$, where $x$ is the number of bots and $y$ is
the indexing time. For the industrial process models, the estimated values for
constant $t$ are 6,065.6, 11,241, 16,735, and 23,071, for 25%, 50%, 75%, 100%
of models in the collection, respectively. The estimated values for
coefficient $k$ are -0.845, -0.834, -0.826, and -0.839, for 25%, 50%, 75%,
100% of models in the industrial collection, respectively. For the synthetic
process models, the estimated values for constant $t$ are 17,991, 35,494,
52,086, and 68,077, for 25%, 50%, 75%, 100% of models in the collection,
respectively. The estimated values for coefficient $k$ are -0.833, -0.806,
-0.827, and -0.834, for 25%, 50%, 75%, 100% of models in the synthetic
collection, respectively. The coefficient of determination $R^{2}$ ranges from
0.9901 to 0.9936 for the industrial process models and from 0.9834 to 0.9884
for the synthetic process models, indicating that the fitted functions can
explain most of the variance in the indexing time.

This experiment also shows that the indexing time grows linearly with the size
of a process model collection. Using one PQL bot, 25% of models in the
industrial collection were indexed in 1 hour and 48 minutes, 50% were indexed
in 3 hours and 22 minutes, 75% in 5 hours and 2 minutes, and the whole
collection was indexed in 6 hours and 54 minutes. This relationship between
the indexing time and the size of the collection is best captured by the
linear function $y=49.549x+158.65$, where $x$ is the number of models in the
collection and $y$ is the indexing time. The coefficient of determination
$R^{2}$ for the above example is 0.9985. The coefficients of determination
$R^{2}$ for the fitted linear functions on four data points range from 0.9985
to 0.9997 (for different numbers of bots). We observed the same trend for the
synthetic collection, with $R^{2}$ values ranging from 0.9949 to 0.9992.

Experiment 1.2: Impact of model size on indexing time. The goal of this
experiment was to assess the impact of size of a model on its indexing time.
The two model collections were indexed three times (using one bot) and for
each model we recorded the average indexing time of the three runs. The bot
was configured to only index the label similarity threshold of 1.0.

Figure 13. Impact of model size on indexing time: (a) industrial models and
(b) synthetic models.

Figure 13 plots the indexing times (in seconds) against different sizes of
workflow systems for (a) the industrial models and (b) the synthetic models.
In this experiment, the size of a workflow system is measured as the number of
its observable transitions; the reason for this is that bots index behavioral
relations over observable transitions. The observed average indexing time of a
model in the industrial collection is 50.3 seconds, with a minimum of 4.0
seconds (for a model with 2 observable transitions) and a maximum of 858.7
seconds (for a model with 25 observable transitions). We have also observed
that 95% of models in the industrial collection can be indexed in less than
200 seconds. The average indexing time of a model in the synthetic collection
is 74.0 seconds, with a minimum of 6.3 seconds (for a model with 3 observable
transitions) and a maximum of 2,465.7 seconds (for a model with 67 observable
transitions). The obtained measurements report that 95% of models in the
synthetic collection can be indexed in less than 250 seconds.

The relation between the indexing time and the model size in the industrial
collection is best approximated by the power function $y=0.8171\times
x^{1.7579}$, which results in a coefficient of determination $R^{2}$ of
0.9915. One obvious outlier workflow system in the industrial collection (a
model with 25 observable transitions whose indexing took 858.7 seconds) can be
explained by the much bigger size of its state space (2,097,422 reachable
states, measured by the LoLA tool) compared to the sizes of state spaces of
the other models in the collection (equal or less than 262,156 reachable
states). For the synthetic models, the relation between the indexing time and
the model size is best explained by the power function $y=0.7423\times
x^{1.7775}$, which results in $R^{2}$ = 0.99.

Given a system, either industrial or synthetic, we have noticed that it can be
classified as an outlier using the value $f(x,y)=x^{2}\times\mathit{log}(y)$,
where $x$ is the number of observable transitions of the system and $y$ is the
size of the state space of the system in terms of the number of its reachable
states. The Pearson’s correlation coefficient between the indexing times and
the values of $f$ is $0.9426$ and $0.9692$ for the industrial and synthetic
models, respectively. The residual analysis has revealed that the four
outliers in the industrial collection are among the six models with the
highest values of $f$, while the seven outliers in the synthetic collection
are among the eight models with the highest values of $f$. The outliers were
identified as models with the standardized residuals beyond $\pm 3$ units. The
four outliers in the industrial collection have 25 (5 minutes and 38 seconds
to index), 25 (14 minutes and 19 seconds), 32 (8 minutes and 48 seconds) and
35 (8 minutes and 48 seconds) observable transitions. Their state spaces
comprise 114,717, 2,097,422, 390, and 882 reachable states, respectively. The
seven outliers in the synthetic collection have 36 (11 minutes and 23 seconds
to index), 36 (10 minutes and 30 seconds), 42 (14 minutes and 58 seconds), 46
(15 minutes and 23 seconds), 56 (27 minutes and 10 seconds), 63 (39 minutes
and 59 seconds), 67 (41 minutes and 6 seconds) observable transitions. Their
state spaces have 303,118, 131,108, 103,694, 1,602, 5,730, 311,306, and 6,818
reachable states, respectively.

Experiment 1.3: Impact of label similarity threshold on indexing time. The
goal of this experiment was to assess the impact of different label similarity
thresholds on the average time required to index a model. In this experiment,
we varied the label similarity threshold (0.5, 0.6, 0.7, 0.8, 0.9 and 1.0)
used to index the models. Both process model collections, i.e., the industrial
and the synthetic, were indexed with one bot three times (for each similarity
threshold), and average indexing times for the three runs were recorded. The
Lucene-VSM label comparison method was used in all the runs, refer to Section
5 for details. The measured average indexing times of an industrial model for
the label similarity thresholds 0.5, 0.6, 0.7, 0.8, 0.9, and 1.0 are 49.73,
50.3, 50.44, 50.48, 50.3, 50.31 seconds, respectively, with the standard
deviation in the range from 80.28 to 81.35 seconds. The measured average
indexing times of a synthetic model for the label similarity thresholds 0.5,
0.6, 0.7, 0.8, 0.9, and 1.0 are 74.53, 74.63, 74.62, 74.57, 74.61, 74.48
seconds, respectively, with the standard deviation in the range from 154.62 to
155.26 seconds.

There is no strong observed relation between the label similarity thresholds
and the measured average indexing times, both for industrial and synthetic
models. We conclude that the impact of different label similarity thresholds
on indexing times is negligible. This can be explained by the small number of
unique labels in both collections (2,278 unique labels across the industrial
models and 10,473 unique labels across the synthetic models) and the fact that
the labels are short character strings (on average 4.84 and 6.08 words in a
label of an industrial and a synthetic model, respectively), whereas modern
information retrieval engines are known to be efficient on collections that
comprise millions of natural language documents of much larger sizes (Baeza-
Yates and Ribeiro-Neto, 2011).

Experiment 1.4: Impact of index size on indexing time. The goal of this
experiment was to measure the impact of index size on the average time
required to index a model. To this end, we randomly split the industrial
collection into four sets of (approximately) the same size (Sets 1–4). Each
set was indexed four times: once when the index was empty, and then after 25%,
50% and 75% of the collection was indexed. In total, we performed four
indexing runs. In the first run, Set 1 was indexed first, followed by indexing
of Set 2, followed by Set 3, and finally concluded by indexing Set 4. The
second run indexed the models in the order of Set 4, Set 1, Set 2, and finally
Set 3. The third run indexed the models in the order of Set 3, Set 4, Set 1,
and finally Set 2. The fourth run indexed the models in the order of Set 2,
Set 3, Set 4, and finally Set 1. In all the runs, the same label similarity
threshold of 1.0 was used. All the four indexing runs were accomplished by one
PQL bot.

For all the sets, we observed that the average indexing time is not
significantly affected by the size of the index. For models in Set 1, the
recorded average indexing times are 53.63 seconds, 53.65 seconds, 54.09
seconds, and 54.26 seconds in the first, second, third, and the fourth run,
respectively. For models in Set 2, the recorded average indexing times are
53.29 seconds, 53.46 seconds, 53.70 seconds, and 53.80 seconds in the first,
second, third, and the fourth run, respectively. For models in Set 3, the
recorded average indexing times are 44.75 seconds, 44.79 seconds, 44.93
seconds, and 45.15 seconds in the first, second, third, and the fourth run,
respectively. Finally, for models in Set 4, the recorded average indexing
times are 49.6 seconds, 49.52 seconds, 49.9 seconds, and 49.92 seconds in the
first, second, third, and the fourth run, respectively. Given any set out of
the four sets of models, the relation between the index size (used as a
starting point to index the given set) and the average indexing time of a
model in the set is best approximated by a polynomial function. The average
indexing time for an industrial model in different sets at different positions
in the indexing queue ranges from 44.75 to 54.26 seconds, with the difference
between the maximum and minimum average indexing time for a given set at
different indexing positions always being within 0.65 seconds. The measured
coefficients of determination are equal to 0.9215, 0.9847, 0.9998, and 0.7366
for Set 1, Set 2, Set 3, and Set 4, respectively. The experiment demonstrates
a general trend of a negligible increase in the indexing time with the growth
of the index size. This observation can be explained by the fact that the
introduced overhead is due to write operations on the PQL index, which can be
efficiently handled by modern database management systems.

In the measurements of the average indexing times for the synthetic collection
we observed a similar trend as in the measurements for the industrial
collection. In particular, given any set out of the four sets of models in the
synthetic collection (note that each set of synthetic models is composed of
250 random models), the relation between the index size (used as a starting
point to index the given set) and the average indexing time of a model in the
set is best approximated by a polynomial function. The average indexing time
for a synthetic model in different sets at different positions in the indexing
queue ranges from 61.7 to 86.74 seconds, with the difference between the
maximum and minimum average indexing time for a given set at different
indexing positions always being within 0.75 seconds. The measured coefficients
of determination are equal to 0.8456, 0.9947, 0.9999, and 0.8545 for Set 1,
Set 2, Set 3, and Set 4, respectively.

###  6.3. Querying Performance

We conducted three experiments to assess the performance of executing
different types of PQL queries. The queries were generated from the templates
discussed in Section 6.1. To conduct the evaluation, for each model collection
and for each template we generated three queries by populating them with
labels randomly selected from all the labels in the collection.

Experiment 2.1: Impact of query threads on querying time. This experiment
measured the impact of the number of query threads and the size of a model
collection on the querying time. We varied the number of query threads (from 1
to 8) and executed all the generated queries on different parts of the
collections (25%, 50%, 75%, and 100% of models in each collection). For each
part of each collection, models were randomly selected three times and the
average querying times for the three runs were recorded. The models were
indexed using the label similarity threshold of 1.0.

Figure 14 plots the querying times (in seconds) for different parts of process
model collections against different numbers of query threads for (a) the
industrial models and (b) the synthetic models. It demonstrates that
additional query threads decrease querying time. As in Experiment 1.1, the
gain in performance gets less pronounced with the increase of the number of
query threads. For example, querying of the industrial models with one thread
took on average 8.259 seconds, two threads managed to accomplish queries over
493 systems in 6.109 seconds (1.35 times faster than using one thread), while
eight thread used 2.037 seconds to execute a query over the whole collection
(four times faster than with one thread). A similar trend can be observed for
the synthetic models.

The relation between the querying time and the number of threads is best
captured by the power function $y=t\times x^{k}$, where $y$ is the querying
time and $x$ is the number of query threads. For the industrial process
models, the estimated values for constant $t$ are 2.0793, 4.1112, 6.3066, and
8.3917, for 25%, 50%, 75%, 100% of models in the collection, respectively. The
estimated values for coefficient $k$ are -0.582, -0.584, -0.595, and -0.594,
for 25%, 50%, 75%, 100% of models in the industrial collection, respectively.
For the synthetic process models, the estimated values for constant $t$ are
4.1811, 8.6902, 13.693, and 19.444, for 25%, 50%, 75%, 100% of models in the
collection, respectively. While the estimated values for coefficient $k$ are
-0.581, -0.597, -0.604, and -0.612, for 25%, 50%, 75%, 100% of models in the
synthetic collection, respectively. The coefficient of determination $R^{2}$
ranges from 0.9969 to 0.9982 for the industrial models and from 0.9983 to
0.9989 for the synthetic models, indicating that the fitted models can explain
most of the variance in the querying time.

The measurements obtained in this experiment can be used to show that the
querying time grows linearly with the size of a process model collection. For
example, the measured average querying time with one query thread over 25% of
the industrial models is 2.037 seconds, over 50% is 4.037 seconds, over 75% is
6.109 seconds, and over the whole collection is 8.259 seconds. This trend is
best described by the linear relation $y=0.0168\times x-0.0658$, where $x$ is
the number of models in the collection and $y$ is the querying time. The
coefficient of determination $R^{2}$ for the above example is 0.9998. The
coefficients of determination $R^{2}$ for the fitted linear functions on four
data points range from 0.9988 to 1.0 (for different numbers of query threads).
We observed the same trend for the synthetic collection, with $R^{2}$ values
ranging from 0.9967 to 0.9998.

Figure 14. Impact of query threads on querying time: (a) industrial models and
(b) synthetic models.

Experiment 2.2: Impact of query types on querying time.

Figure 15. The average querying times for different model collection sizes
(a,c,e,g) and for different numbers of query threads (b,d,f,h); PQL queries in
Cats. 1 and 2 for the industrial models (a,b) and for the synthetic models
(e,f), and PQL queries in Cat. 3 for the industrial models (c,d) and for the
synthetic models (g,h).

This experiment aimed to assess the impact of different query types on
querying time. It uses the same setup as Experiment 2.1. In this experiment,
we measured querying times for different query groups discussed in Section
6.1.

Figs. 15 and 15 show the average querying times for the collection of
industrial models for queries in Categories 1 and 2, while Figs. 15 and 15
show the average querying times for queries in Category 3. The average
querying times for the synthetic collection are shown in Figs. 15 and 15
(Categories 1 and 2) and Figs. 15 and 15 (Category 3). Queries in Category 1
only comprise atomic predicates and, thus, are the fastest. The measured
average querying time for the Category 1 queries using one query thread is
1.75 seconds for the 493 models in the industrial collection (approximately
3.5ms per one model-query check) and 4.84 seconds for the 1,000 models in the
synthetic collection (approximately 4.8ms per one model-query check). With
eight query threads, the Category 1 queries were on average accomplished in
0.47 seconds for the 493 models in the industrial collection and 1.61 seconds
for the 1,000 models in the synthetic collection. Queries in Category 2
comprise atomic predicates and logical connectives. Thus, they require a bit
more time to accomplish than queries in Category 1. The measured average
querying time for Category 2 queries with one thread is 2.8 seconds for the
industrial models and 8.2 seconds for the synthetic models. With eight query
threads, it is 0.84 and 2.52 seconds for the industrial and synthetic models,
respectively. Queries in Category 3 comprise macros and, hence, are the
lengthiest. The measured average querying time for Category 3 queries with one
query thread is 10.89 seconds for the industrial models (approximately 11ms
per one model-query check) and 24.76 seconds for the synthetic models
(approximately 25ms per one model-query check). With eight query threads, it
is 3.23 and 6.96 seconds for the industrial and synthetic models,
respectively.

Figs. 15, 15, 15 and 15 demonstrate the linear dependency between the number
of models in a collection and querying time for different query types. The
coefficients of determination $R^{2}$ for the fitted linear functions for
different query subgroups range from 0.9718 to 1.0 for the industrial models
and from 0.9592 to 0.9992 for the synthetic models. Finally, Figs. 15, 15, 15,
and 15 show that for all the query subgroups the relation between the querying
time and the number of query threads follows the trend observed in Experiment
2.1. The coefficients of determination $R^{2}$ for the fitted power functions
for different query subgroups range from 0.9724 to 0.998 for the industrial
models and from 0.9329 to 0.9955 for the synthetic models.

Experiment 2.3: Impact of label similarity on querying time. The aim of this
experiment was to measure the impact of label similarity on querying time. To
this end, we repeated Experiment 2.1 with the following modifications: (i) the
bots were configured to index label similarity thresholds of 0.75 and 1.0,
(ii) all the query templates were augmented to include the “tilde” symbol
immediately before every activity label (thus, similar labels were considered
during querying), and (iii) the tool was configured to use a default label
similarity threshold of 0.75.

We compared the measured querying times with the querying times obtained in
Experiment 2.1. For the industrial process models, the querying times (using
one query thread) on average are 10.9% higher for queries that account for
similar labels. For the synthetic process models, the querying times (again,
using one query thread) on average are 9.47% higher for queries that account
for similar labels. This small overhead can be explained by the fact that the
PQL tool indexes behavioral relations at the level of PQL tasks and, thus, at
runtime, the overhead is only due to the additional time required to retrieve
information on the indexed PQL tasks.

##  7\. Related Work

Recently, we conducted a systematic literature review of the state of the art
methods for querying process repositories (Polyvyanyy et al., 2017). As part
of that study, we designed a framework for developing process querying
methods. The framework is an abstract system in which components can be
selectively replaced to result in a new process querying method. According to
this framework, PQL addresses querying of _formal_ process models using a
query language with a _formal_ semantics that implements the _read_ querying
intent, i.e., is designed to retrieve models from repositories. Two recent
surveys of process querying methods (Wang et al., 2014; Polyvyanyy et al.,
2017) confirm that query languages with these characteristics constitute a gap
in the area of process querying. In (Polyvyanyy, 2018), we categorized and
summarized the existing process querying methods. According to that
classification, two prominent existing works for behavioral querying of
process models that share similar characteristics with PQL are the works on
“Behavior Query Language” (BQL) (Jin et al., 2011) and “A Process-model Query
Language” (APQL) (ter Hofstede et al., 2013). Next, we briefly review APQL and
BQL, summarize some important results on behavioral predicates, and discuss
several related techniques from the areas outside process querying.

Behavioral querying. PQL is inspired by our work on APQL and redesigns APQL in
many respects. PQL differs from APQL in that it is grounded in a different and
empirically justified collection of behavioral predicates, extends the
abstract syntax of APQL, proposes a concrete syntax, has an implementation
that demonstrates its feasibility, and operates on the level of observable
behaviors, i.e., incorporates mechanisms for interpreting two different tasks
as such that have the same meaning for the purpose of evaluating the queries.
If compared with BQL, PQL is rigorous since both the syntax and semantics of
the language are formally defined. BQL is grounded in three behavioral
predicates. All these predicates belong to the 4C spectrum and were included
in our empirical study. These three predicates are Conflict (called “exclude”
in (Jin et al., 2011)), ExistCausal (“precede”), and ExistConcurrent
(“parallel with”), refer to Section 4.1.1 for more details. As a result of our
empirical evaluation, only one of these three predicates, namely Conflict, was
selected to be included in the set of eight core PQL predicates. As to
ExistCausal and ExistConcurrent, the stakeholders have given their preference
to “stronger” predicates of TotalCausal and TotalConcurrent, which ensure that
the respective behavioral relation holds for all (rather than only for some)
occurrences of the tasks. Finally, the fundamental difference between PQL and
BQL is that BQL predicates are defined over occurrences of tasks, while PQL
predicates are defined over aggregations (derived using quantification) over
the occurrences of tasks.

Model Checking. Model checking studies problems that can verify various
properties of process models (Chan et al., 1998; Baier and Katoen, 2008). A
model checking problem is a problem that, given a formal specification of a
property, usually captured using some _specification language_ , and a process
model, answers whether the property holds in the given model. Often, in order
to solve the problem, a model checking technique proceeds by constructing an
alternative representation of the model that indicates whether the given
property holds or not in the model. Model checking techniques usually use
_temporal logics_ as property specification languages, e.g., linear temporal
logic (LTL) and computational tree logic (CTL). Model checking techniques can
be employed for process querying to retrieve process models that fulfill a
given property (Gurfinkel et al., 2003).

As recently demonstrated by Wolf (Wolf, 2018), computations of most of the 4C
behavioral relations can be reduced, via non-trivial transformations that
require exponential space, to classical interleaving-based model checking
problems. Only one problem remains completely unsolved, whereas several
problems were solved in the absence of auto-concurrency. In fact, based on the
results reported in (Polyvyanyy et al., 2014b; Wolf, 2018), we know that all
the predicates selected for inclusion into PQL, refer to Section 4.1.3, can be
reduced to model checking problems. However, one cannot directly apply the
proposed solutions for process querying. Note that the proposed in (Wolf,
2018) LTL and CTL properties for computing the 4C relations are formulated
over the transformed models and, hence, do not convey the meanings of the
properties to be computed, which makes them unsuitable for the user
interpretations. Also, the performance of the approach proposed in (Wolf,
2018) has not been evaluated; note that model checking on infinite-state
systems is undecidable and is PSPACE-complete on finite state systems (Esparza
and Nielsen, 1994). Such an evaluation, and development of new efficient
techniques for computing the 4C relations, may contribute to the development
of PQL.

Behavioral predicates. In (Dwyer et al., 1999), the authors report the results
of a survey of property specifications (a.k.a. behavioral predicates) captured
in _temporal logics_ , e.g., LTL or CTL. The authors collected and classified
555 properties, most of which are specified in LTL, from a wide range of
domains, including hardware protocols, communication protocols, avionics,
operating systems, and database systems. Interestingly, the authors conclude
that “even with significant expertise, dealing with the complexity of such a
specification [a temporal logic property] can be daunting” and suggest that
often “complexity is addressed by the definition and use of abstraction”. PQL
implements such an abstraction. There are no translations from PQL predicates
to temporal logic properties over concepts of the original process model, see
above. However, it is easy to see that several properties surveyed in (Dwyer
et al., 1999) can be expressed as logical expressions over the 4C spectrum
relations. A comprehensive study of such translations is an interesting
direction to explore.

To the best of our knowledge, there are no existing works that study the
relevance of behavioral predicates for the purpose of querying (business)
process models. Future empirical studies will aim at gaining a better
understanding of the suitability of behavioral predicates for process
querying, as per the process querying compromise between decidable,
efficiently computable, and suitable process querying methods (Polyvyanyy et
al., 2017).

Verification of software systems. In (Dwyer et al., 2004), the authors
proposed FLAVERS—a finite-state verification technique to analyze whether a
concurrent software system satisfies a given user-specified property. To
perform the verification, FLAVERS constructs an abstract representation of the
system. This abstraction step comes at a price of precision of the analysis
results. In our work, we suggest using PQL to query repositories of business
process models. However, one can explore PQL for querying, testing, and
verification of software systems. Unlike FLAVERS, PQL is precise, i.e., the
result of every PQL query is free from false positive and false negative
errors. FLAVERS and PQL differ in how they interpret models of analyzed
models, according to the interleaving and noninterleaving semantics of
concurrent systems (Sassone et al., 1996), respectively. Thus, PQL can be used
to express properties that address potential simultaneous execution of
instructions of software systems.

In software engineering, well-established finite-state verification
techniques, like the methods based on classical model checking or the FLAVERS
technique, are used to inform continuous improvement of processes (Clarke et
al., 2008; Osterweil et al., 2017). PQL can enrich this repertoire of
verification techniques for detecting errors in semantically rich process
models with user interpretable and relevant properties.

Declarative process discovery. Process mining assists business analysts in
dealing with the emerging complexities and uncertainties introduced by
business processes, as it aims to discover, monitor and improve processes
observed in the real world using the knowledge accumulated in event logs
produced by modern information systems (van der Aalst, 2016). An event log is
a collection of traces, each representing events executed by a business
process. The process discovery problem consists of obtaining a good process
model that describes the behavior recorded in a given event log. Declarative
process discovery aims to construct such process models as collections of
declarative constraints over possible executions of business activities. These
declarative constraints are often expressed as behavioral predicates, similar
to those used in PQL.

In (Ciccio and Mecella, 2015), the authors proposed an algorithm for
declarative process discovery, called MINERful. The algorithm performs the
statistical analysis of the input event log, and then uses the derived
knowledge to compose the declarative constraints which collectively describe
the traces recorded in the event log. In particular, MINERful discovers
Declare constraints (van der Aalst et al., 2009), which is a particular
repertoire of 20 LTL templates. In (Westergaard et al., 2013), the authors
propose another algorithm capable of discovering Declare constraints from
event logs, called UnconstrainedMiner. To address the problem of LTL semantics
over finite traces, in that work, Declare templates are translated to regular
expressions.

Next generation declarative process discovery algorithms can target discovery
of the 4C spectrum constraints, in general, and PQL predicates, in particular.
This will allow overcoming two limitations of the existing techniques: the
inability of encoding noninterleaving semantics (Sassone et al., 1996) and
lack of empirical justification of the discovered constraints.

##  8\. Conclusion

This paper proposed a query language for retrieving models from process model
repositories. The language has an _SQL-like syntax_ to facilitate ease of use
and its basic predicates are _empirically grounded_. Noteworthy is also the
fact that the language targets process _behavior_ rather than structural
aspects of process models. This focus on the behavior seems more natural than
the usual way of querying the representations of the behavior. The language
supports label similarity, i.e., labels are assessed as to whether they are
sufficiently similar (which is determined with respect to a given threshold)
to another label. Support for this feature is essential as variations on task
names can easily emerge when a range of people are involved in the creation of
process models.

The proposed query language has been implemented and its runtime performance
evaluated using real-life and synthetic process models. The conducted
experiments indicate the feasibility of computing the basic PQL predicates and
demonstrate that the implemented PQL Tools can execute PQL queries in almost
real-time.

There are several limitations of this work that should be acknowledged. Some
of these limitations naturally give rise to possible avenues for future work.

First of all, the expressiveness of the proposed query language is constrained
by the choice of basic predicates. As it turns out though, this is a
fundamental limitation that no semantic process model query language grounded
in behavioral predicates can escape (Polyvyanyy et al., 2016). Expressiveness
can be extended, for instance, by allowing the use of example executions in
queries, in particular executions that contain wildcards to express search
intents like “find all process models that allow the execution
$\left\langle\texttt{a},\texttt{b},*,\texttt{b},\texttt{b},*,\texttt{c},*\right\rangle$”.
Through the use of wildcards one can search for those process models in which
_any_ trace that fits the template can be executed.

Second, the proposed design of PQL, and the design of its subsequent versions,
should be justified by new empirical evidence. For example, it is important to
study the ratio between the queries that users want to express and PQL can
support and to improve the language accordingly. One can conduct empirical
studies to assess how simple it is for the users to specify complex behavioral
queries, and use the obtained insights to simplify the language. As another
example, one can empirically assess the usefulness of the proposed exploratory
search principle.

Third, the proposed query language is only concerned with control-flow aspects
of process models and does not take the data and resource perspectives into
account. The potential use of the query language can be widened by allowing
queries that refer to aspects other than control-flow.

Fourth, PQL can be extended with functionality that is auxiliary to behavioral
querying, e.g., aggregate functions over retrieved processes. PQL predicates
operate over the global process scope, i.e., over processes that represent
completed executions of process models. Similar to some properties surveyed by
Dwyer et al. (Dwyer et al., 1999), PQL predicates can be generalized to
operate over other scopes, e.g., between given process conditions. However, it
is worth mentioning that 80% of the surveyed in (Dwyer et al., 1999)
properties address the global scope.

Fifth, PQL can be extended with manipulation statements (think INSERT, DELETE,
UPDATE). Through the use of these statements, it should be possible to add,
delete, and modify process models.

Another limitation concerns the requirement that the class of process models
that the query language can deal with is the class of sound workflow systems.
In practice, process models may not always be sound, for example as models may
not yet have been completed, and it is worthwhile to explore how the current
work could be adapted to allow for a wider class of process models.

Despite the benefits of a query language based on the behavior described in
models, there is a drawback that the behavioral aspects can be complex and
consequently query results may not always be intuitive to stakeholders. To
facilitate query understanding, process models can be annotated to explain the
reasons for their inclusion in the query results.

Acknowledgements

We would like to thank Jan Recker for his input in the design of the
experiment on assessing practical relevance of using behavioral predicates for
querying process repositories.

## References

  * (1)
  * Aho and Ullman (1992) Alfred Aho and Jeffrey Ullman. 1992.  _Foundations of Computer Science_.  W.H. Freeman and Company.
  * Awad (2007) Ahmed Awad. 2007\.  BPMN-Q: A Language to Query Business Processes. In _Enterprise Modelling and Information Systems Architectures - Concepts and Applications , Proceedings of the 2nd International Workshop on Enterprise Modelling and Information Systems Architectures (EMISA’07), St. Goar, Germany, October 8-9, 2007_. 115–128.  http://subs.emis.de/LNI/Proceedings/Proceedings119/article1957.html
  * Awad et al. (2008) Ahmed Awad, Artem Polyvyanyy, and Mathias Weske. 2008\.  Semantic Querying of Business Process Models. In _Enterprise Distributed Object Computing Conference (EDOC)_. IEEE Computer Society, 85–94.
  * Baeza-Yates and Ribeiro-Neto (2011) Ricardo A. Baeza-Yates and Berthier A. Ribeiro-Neto. 2011\.  _Modern Information Retrieval—The Concepts and Technology Behind Search_ (2 ed.).  Pearson Education Ltd., Harlow, England.
  * Baier and Katoen (2008) Christel Baier and Joost-Pieter Katoen. 2008.  _Principles of Model Checking_.  MIT Press.
  * Beeri et al. (2005) Catriel Beeri, Anat Eyal, Simon Kamenkovich, and Tova Milo. 2005\.  Querying Business Processes with BP-QL. In _Proceedings of the 31st International Conference on Very Large Data Bases, Trondheim, Norway, August 30 - September 2, 2005_. ACM, 1255–1258.  http://www.vldb.org/conf/2005/papers/p1255-beeri.pdf
  * Billington et al. (2003) Jonathan Billington, Søren Christensen, Kees M. van Hee, Ekkart Kindler, Olaf Kummer, Laure Petrucci, Reinier Post, Christian Stehno, and Michael Weber. 2003\.  The Petri Net Markup Language: Concepts, Technology, and Tools. In _Applications and Theory of Petri Nets 2003, 24th International Conference, ICATPN 2003, Eindhoven, The Netherlands, June 23–27, 2003, Proceedings_ _(Lecture Notes in Computer Science)_ , Wil M.P. van der Aalst and Eike Best (Eds.), Vol. 2679. Springer, 483–505.
  * Chamberlin and Boyce (1974) Donald D. Chamberlin and Raymond F. Boyce. 1974.  SEQUEL: A Structured English Query Language. In _ACM SIGMOD Workshop_. 249–264.
  * Chan et al. (1998) William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon Damon Reese. 1998.  Model Checking Large Software Specifications.  _IEEE Trans. Software Eng._ 24, 7 (1998), 498–520.
  * Ciccio and Mecella (2015) Claudio Di Ciccio and Massimo Mecella. 2015.  On the Discovery of Declarative Control Flows for Artful Processes.  _ACM Transactions on Management Information Systems_ 5, 4 (jan 2015), 24:1–24:37.  https://doi.org/10.1145/2629447
  * Clarke et al. (2008) Lori A. Clarke, George S. Avrunin, and Leon J. Osterweil. 2008\.  Using software engineering technology to improve the quality of medical processes. In _30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, Companion Volume_ , Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn (Eds.). ACM Press, 889–898.  https://doi.org/10.1145/1370175.1370179
  * Curran et al. (1998) Thomas Curran, Gerhard Keller, and Andrew Ladd. 1998\.  _SAP R/3 Business Blueprint: Understanding the Business Process Reference Model_.  Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
  * Date and Darwen (1996) C.J. Date and Hugh Darwen. 1996.  _A Guide to the SQL Standard: A User’s Guide to the Standard Database Language SQL_ (4 ed.).  Addison-Wesley.
  * Davis (1989) Fred D. Davis. 1989\.  Perceived Usefulness, Perceived Ease of Use, and User Acceptance of Information Technology.  _MIS Quarterly_ 13, 3 (1989), 319–340.
  * Dijkman et al. (2008) Remco M. Dijkman, Marlon Dumas, and Chun Ouyang. 2008\.  Semantics and Analysis of Business Process Models in BPMN.  _Information & Software Technology_ 50, 12 (2008), 1281–1294.  https://doi.org/10.1016/j.infsof.2008.02.006
  * Dumas et al. (2013) Marlon Dumas, Marcello La Rosa, Jan Mendling, and Hajo A. Reijers. 2013.  _Fundamentals of Business Process Management_.  Springer.
  * Dwyer et al. (1999) Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1999.  Patterns in Property Specifications for Finite-State Verification. In _Proceedings of the 1999 International Conference on Software Engineering, ICSE’ 99, Los Angeles, CA, USA, May 16–22, 1999._ , Barry W. Boehm, David Garlan, and Jeff Kramer (Eds.). ACM Press, 411–420.  https://doi.org/10.1145/302405.302672
  * Dwyer et al. (2004) Matthew B. Dwyer, Lori A. Clarke, Jamieson M. Cobleigh, and Gleb Naumovich. 2004.  Flow Analysis for Verifying Properties of Concurrent Software Systems.  _ACM Transactions on Software Engineering and Methodology (TOSEM)_ 13, 4 (Oct. 2004), 359–430.  https://doi.org/10.1145/1040291.1040292
  * Engelfriet (1991) Joost Engelfriet. 1991\.  Branching Processes of Petri Nets.  _Acta Informatica_ 28, 6 (1991), 575–591.  https://doi.org/10.1007/BF01463946
  * Esparza and Heljanko (2008) Javier Esparza and Keijo Heljanko. 2008.  _Unfoldings—A Partial-Order Approach to Model Checking_.  Springer.  https://doi.org/10.1007/978-3-540-77426-6
  * Esparza and Nielsen (1994) Javier Esparza and Mogens Nielsen. 1994.  Decidability Issues for Petri Nets—A Survey.  _Bulletin of the EATCS_ 52 (1994), 244–262.
  * Esparza et al. (2002) Javier Esparza, Stefan Römer, and Walter Vogler. 2002\.  An Improvement of McMillan’s Unfolding Algorithm.  _Formal Methods in System Design (FMSD)_ 20, 3 (2002), 285–310.
  * Fahland et al. (2011) Dirk Fahland, Cédric Favre, Jana Koehler, Niels Lohmann, Hagen Völzer, and Karsten Wolf. 2011\.  Analysis on Demand: Instantaneous Soundness Checking of Industrial Business Process Models.  _Data & Knowledge Engineering (DKE)_ 70, 5 (2011), 448–466.  https://doi.org/10.1016/j.datak.2011.01.004
  * Faul et al. (2009) Franz Faul, Edgar Erdfelder, Axel Buchner, and Albert-Georg Lang. 2009.  Statistical power analyses using G*Power 3.1: Tests for correlation and regression analyses.  _Behavior Research Methods_ 41, 4 (2009), 1149–1160.  https://doi.org/10.3758/BRM.41.4.1149
  * Goltz and Reisig (1983) Ursula Goltz and Wolfgang Reisig. 1983.  The Non-sequential Behavior of Petri Nets.  _Information and Control (IANDC)_ 57, 2/3 (1983), 125–147.
  * Gurfinkel et al. (2003) Arie Gurfinkel, Marsha Chechik, and Benet Devereux. 2003\.  Temporal Logic Query Checking: A Tool for Model Exploration.  _IEEE Trans. Software Eng._ 29, 10 (2003), 898–914.
  * Haar et al. (2013) Stefan Haar, Christian Kern, and Stefan Schwoon. 2013\.  Computing the Reveals Relation in Occurrence Nets.  _Theoretical Computer Science (TCS)_ 493 (2013), 66–79.  https://doi.org/10.1016/j.tcs.2013.04.028
  * Hack (1975) Michel Hack. 1975\.  _Decidability Questions for Petri Nets_.  Garland Publishing, New York.
  * Hoare (1973) C.A.R. Hoare. 1973\.  _Hints on Programming Language Design._ Technical Report. Stanford, CA, USA.
  * Hopcroft et al. (2006) John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006\.  _Introduction to Automata Theory, Languages, and Computation_ (3 ed.).  Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
  * Jin et al. (2011) Tao Jin, Jianmin Wang, and Lijie Wen. 2011.  Querying Business Process Models Based on Semantics. In _DASFAA_. Springer, 164–178.