Repairing Soundness Properties in Data-Aware Processes

This page contains supporting material for the paper Repairing Soundness Properties in Data-Aware Processes by Paolo Felli, Marco Montali, and Sarah Winkler, submitted to ICPM 2023.

Links related to the tool

Results

  process source input file DDSA repair type time iterations repaired DDSA
(A1) road fines normative [1, Fig.7] pnml png restrict 50s 2 png
          extend 71s 2 png
(A2) road fines mined [2, Fig.12.7] pnml png restrict 24s 1 png
          extend 22s 1 png
(A3) digital whiteboard: transfer [2, Fig.14.3] pnml png restrict 2.1s 1 png
          extend 3s 1 png
(A4) package handling [5, Fig.5] pnml png restrict 6s 0 png
          extend 6s 0 png
(A5) auction [4, Ex. 1.1] pnml png restrict 8s 1 png
          extend 20s 1 png
(A6) simple auction [3, Fig. 3] pnml png restrict 2.5s 1 png
          extend 2.7s 1 png
(A7) simple auction with reset [3, Fig. 3] pnml png restrict 2.3s 1 png
          extend 2.3s 1 png
(B1) credit approval [5,Fig. 3] modified pnml png restrict 2.1s 1 png
          extend 2.4s 1 png
(C1) livelock pnml png restrict 2.1s 1 png
          extend 2.4s 1 png
(C2) non-exhaustive choice json png restrict 2.2s 1 png
          extend 2.4s 1 png
(C3) non-exhaustive choice for type reasons json png restrict 2.1s 1 png
          extend 2.2s 1 png
(C4) single-variable livelock json png restrict 2.3s 1 png
          extend 2.3s 1 png
(C5) even/odd json png restrict 2.9s 0 png
          extend 2.9s 0 png
(C6) dead loop json png restrict 2.2s 0 png
          extend 2.2s 0 png
(C7) shopping with 1000$ json png restrict 22s 1 png
          extend 12.7s 1 png
(C8) exponential growth, one level pnml png restrict 2.5s 2 png
          extend 2.7s 2 png
(C9) exponential growth, two levels pnml png restrict 3.2s 7 png
          extend 3s 6 png
(C10) exponential growth, three levels pnml png restrict 7s 15 png
          extend 6.2s 14 png
(C11) exponential growth, four levels pnml png restrict 48s 31 png
          extend 32s 30 png
The DPNs (A1)-(A7) are taken from the below references and were recognized data-aware unsound in earlier work [3]. DPNs (C1)-(C10) are crafted, syntactical examples. DPNs (B1) are taken from the literature but were modified to exhibit data-aware unsoundness.

References:

  • [1] Mannhardt, F., de Leoni, M., Reijers, H., van der Aalst, W.: Balanced multi-perspective checking of process conformance. Computing 98(4), 407-437 (2016)
  • [2] Mannhardt, F.: Multi-perspective Process Mining. Ph.D. thesis, Technical University of Eindhoven (2018)
  • [3] Felli, P., de Leoni, M., Montali, M.: Soundness verification of data-aware process models with variable-to-variable conditions. Fundamenta Informaticae 182(1), 1-29 (2021)
  • [4] Felli, P., Montali, M., Winkler, S.: Linear-time verification of data-aware dynamic systems with arithmetic. In: Proc. 36th AAAI. pp. 5642-5650. AAAI Press (2022)
  • [5] de Leoni, M., Mannhardt, F.: Decision discovery in business processes. In: Encyclopedia of Big Data Technologies, pp. 1–12. Springer (2018)