Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Invertible State Space for Process Trees

Gero Kolhof, Sebastiaan J. van Zelst

TL;DR

This work introduces an invertible state-space framework for process trees by modeling each vertex with three states ($F$, $O$, $C$) and defining a rigorous set of transitions. It proves that the state-space graph $RG(T)$ is isomorphic to $RG(T^{-1})$, enabling effective bidirectional search and facilitating decomposition-based strategies. The authors implement reduction techniques such as fast-forwarding and avoidance of meaningless $F\leftrightarrow C$ alternations, and demonstrate substantial memory and time savings over unidirectional search, especially on larger state spaces. Parallel bidirectional search (BDP) yields further speedups. These results lay the groundwork for efficient algorithms in process-tree analysis, including conformance checking and alignment computation, by leveraging bidirectional search in an invertible state-space setting.

Abstract

Process models are, like event data, first-class citizens in most process mining approaches. Several process modeling formalisms have been proposed and used, e.g., Petri nets, BPMN, and process trees. Despite their frequent use, little research addresses the formal properties of process trees and the corresponding potential to improve the efficiency of solving common computational problems. Therefore, in this paper, we propose an invertible state space definition for process trees and demonstrate that the corresponding state space graph is isomorphic to the state space graph of the tree's inverse. Our result supports the development of novel, time-efficient, decomposition strategies for applications of process trees. Our experiments confirm that our state space definition allows for the adoption of bidirectional state space search, which significantly improves the overall performance of state space searches.

An Invertible State Space for Process Trees

TL;DR

This work introduces an invertible state-space framework for process trees by modeling each vertex with three states (, , ) and defining a rigorous set of transitions. It proves that the state-space graph is isomorphic to , enabling effective bidirectional search and facilitating decomposition-based strategies. The authors implement reduction techniques such as fast-forwarding and avoidance of meaningless alternations, and demonstrate substantial memory and time savings over unidirectional search, especially on larger state spaces. Parallel bidirectional search (BDP) yields further speedups. These results lay the groundwork for efficient algorithms in process-tree analysis, including conformance checking and alignment computation, by leveraging bidirectional search in an invertible state-space setting.

Abstract

Process models are, like event data, first-class citizens in most process mining approaches. Several process modeling formalisms have been proposed and used, e.g., Petri nets, BPMN, and process trees. Despite their frequent use, little research addresses the formal properties of process trees and the corresponding potential to improve the efficiency of solving common computational problems. Therefore, in this paper, we propose an invertible state space definition for process trees and demonstrate that the corresponding state space graph is isomorphic to the state space graph of the tree's inverse. Our result supports the development of novel, time-efficient, decomposition strategies for applications of process trees. Our experiments confirm that our state space definition allows for the adoption of bidirectional state space search, which significantly improves the overall performance of state space searches.
Paper Structure (14 sections, 3 theorems, 9 equations, 7 figures, 1 table)

This paper contains 14 sections, 3 theorems, 9 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Notation
  3. Process Trees
  4. An Invertible State Space
  5. States and Transitions
  6. State Inverse and State Space Isomorphism
  7. State Space Reduction
  8. State Matching
  9. Evaluation
  10. Experimental Setup
  11. Results
  12. Threats to Validity
  13. Related Work
  14. Conclusion

Key Result

Lemma 1

Let $T{=}(V,E,r,\ell)$ be a process tree and let $T^{-1}{=}(V,E,r,\ell')$ be its inverse. Let $S{=}\{F,O,C\}$, let $s_1,s_2{\in}\mathcal{R}(T, \vec{F})$ be two reachable process tree states. Let $v{\in}V$ and let $X,Y{\in}S$. $(T,s_1){\xrightarrow{v[X{\to}Y]}}(T,s_2){\Leftrightarrow}(T^{-1},s_2^{-1}

Figures (7)

  • Figure 1: Example process tree $T_1$, written in short-hand notation as: $\to(a,b,+(\circlearrowleft(\leftarrow(\times(c,\tau),d),e),f),g)$.
  • Figure 2: Feasible vertex states and the allowed transitions.
  • Figure 3: Schematic overview of the state spaces of simple binary process trees (in black) and their inverses (in gray). Straight arcs ($\to$) represent single transitions; wobbly arcs ($\leadsto$) represent multiple transitions. States are mapped to their inverse in the inverse state space using red undirected wobbly edges. The patterns are easily extended to trees with an arbitrary number of children.
  • Figure 4: Schematic example of the need for the alternating property, applied to $v_2$, i.e., $v_2[F{\to}C]$ and $v_2[C{\to}F]$
  • Figure 5: Reduction factor of the memory consumption and execution time of BD and BDP compared to UD.
  • ...and 2 more figures

Theorems & Definitions (9)

  • Definition 1: Process Tree
  • Definition 2: Process Tree Language
  • Definition 3: Process Tree Inverse
  • Definition 4: Process Tree State
  • Definition 5: Legal Transition
  • Definition 6: Process Tree State Inverse
  • Lemma 1: Transition Inversibility
  • Corollary 1: State Space Isomorphism
  • Corollary 2: Language Equivalence