Symbolically Aligning Observed and Modelled Behaviour

Vincent Bloemen, Jaco van de Pol, W.M.P. van der Aalst

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)
32 Downloads (Pure)

Abstract

Conformance checking is a branch of process mining that aims to assess to what degree a given set of log traces and a corresponding reference model conform to each other. The state-of-the-art approach in conformance checking is based on the concept of alignments. Alignments express the observed behaviour in terms of the reference model while minimizing the number of mismatches between the event data and the model. The currently known best algorithm for constructing alignments applies the A* shortest path algorithm for each trace of event data. In this work, we apply insights from the field of model checking to aid conformance checking. We investigate whether alignments can be computed efficiently via symbolic reachability with decision diagrams. We designed a symbolic algorithm for computing shortest-paths on graphs restricted to 0- and 1-cost edges (which is typical for alignments). We have implemented our approach in the LTSmin model checking toolset and compare its performance with the A* implementation supported by ProM. We generated more than 4000 experiments (Petri net model and log trace combinations) by setting various parameters, and analysed performance and related these to structural properties. Our empirical study shows that the symbolic technique is in general better suited for computing alignments on large models than the A* approach. Our approach is better performing in cases where the size of the state-space tends to blow up. Based on our experiments we conclude that the techniques are complementary, since there is a significant number of cases where A* outperforms the symbolic technique and vice versa.
Original languageEnglish
Title of host publication2018 18th International Conference on Application of Concurrency to System Design
Subtitle of host publicationProceedings
PublisherIEEE
Pages50-59
Number of pages10
ISBN (Electronic)978-1-5386-7013-2
ISBN (Print)978-1-5386-7013-2
DOIs
Publication statusPublished - 25 Jun 2018
Event18th International Conference on Application of Concurrency to System Design 2018 - Bratislava, Slovakia
Duration: 24 Jun 201829 Jun 2018
Conference number: 18
https://interes.institute/acsd2018/

Conference

Conference18th International Conference on Application of Concurrency to System Design 2018
Abbreviated titleACSD 2018
CountrySlovakia
CityBratislava
Period24/06/1829/06/18
Internet address

Fingerprint

Model checking
Petri nets
Structural properties
Experiments
Costs

Keywords

  • conformance checking
  • process mining
  • model checking
  • symbolic reachability
  • alignment
  • algorithm
  • graph search

Cite this

Bloemen, V., van de Pol, J., & van der Aalst, W. M. P. (2018). Symbolically Aligning Observed and Modelled Behaviour. In 2018 18th International Conference on Application of Concurrency to System Design : Proceedings (pp. 50-59). IEEE. https://doi.org/10.1109/ACSD.2018.00008
Bloemen, Vincent ; van de Pol, Jaco ; van der Aalst, W.M.P. / Symbolically Aligning Observed and Modelled Behaviour. 2018 18th International Conference on Application of Concurrency to System Design : Proceedings. IEEE, 2018. pp. 50-59
@inbook{2ad5702971424c13bc687cdb1d6153be,
title = "Symbolically Aligning Observed and Modelled Behaviour",
abstract = "Conformance checking is a branch of process mining that aims to assess to what degree a given set of log traces and a corresponding reference model conform to each other. The state-of-the-art approach in conformance checking is based on the concept of alignments. Alignments express the observed behaviour in terms of the reference model while minimizing the number of mismatches between the event data and the model. The currently known best algorithm for constructing alignments applies the A* shortest path algorithm for each trace of event data. In this work, we apply insights from the field of model checking to aid conformance checking. We investigate whether alignments can be computed efficiently via symbolic reachability with decision diagrams. We designed a symbolic algorithm for computing shortest-paths on graphs restricted to 0- and 1-cost edges (which is typical for alignments). We have implemented our approach in the LTSmin model checking toolset and compare its performance with the A* implementation supported by ProM. We generated more than 4000 experiments (Petri net model and log trace combinations) by setting various parameters, and analysed performance and related these to structural properties. Our empirical study shows that the symbolic technique is in general better suited for computing alignments on large models than the A* approach. Our approach is better performing in cases where the size of the state-space tends to blow up. Based on our experiments we conclude that the techniques are complementary, since there is a significant number of cases where A* outperforms the symbolic technique and vice versa.",
keywords = "conformance checking, process mining, model checking, symbolic reachability, alignment, algorithm, graph search",
author = "Vincent Bloemen and {van de Pol}, Jaco and {van der Aalst}, W.M.P.",
year = "2018",
month = "6",
day = "25",
doi = "10.1109/ACSD.2018.00008",
language = "English",
isbn = "978-1-5386-7013-2",
pages = "50--59",
booktitle = "2018 18th International Conference on Application of Concurrency to System Design",
publisher = "IEEE",
address = "United States",

}

Bloemen, V, van de Pol, J & van der Aalst, WMP 2018, Symbolically Aligning Observed and Modelled Behaviour. in 2018 18th International Conference on Application of Concurrency to System Design : Proceedings. IEEE, pp. 50-59, 18th International Conference on Application of Concurrency to System Design 2018, Bratislava, Slovakia, 24/06/18. https://doi.org/10.1109/ACSD.2018.00008

Symbolically Aligning Observed and Modelled Behaviour. / Bloemen, Vincent ; van de Pol, Jaco; van der Aalst, W.M.P.

2018 18th International Conference on Application of Concurrency to System Design : Proceedings. IEEE, 2018. p. 50-59.

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

TY - CHAP

T1 - Symbolically Aligning Observed and Modelled Behaviour

AU - Bloemen, Vincent

AU - van de Pol, Jaco

AU - van der Aalst, W.M.P.

PY - 2018/6/25

Y1 - 2018/6/25

N2 - Conformance checking is a branch of process mining that aims to assess to what degree a given set of log traces and a corresponding reference model conform to each other. The state-of-the-art approach in conformance checking is based on the concept of alignments. Alignments express the observed behaviour in terms of the reference model while minimizing the number of mismatches between the event data and the model. The currently known best algorithm for constructing alignments applies the A* shortest path algorithm for each trace of event data. In this work, we apply insights from the field of model checking to aid conformance checking. We investigate whether alignments can be computed efficiently via symbolic reachability with decision diagrams. We designed a symbolic algorithm for computing shortest-paths on graphs restricted to 0- and 1-cost edges (which is typical for alignments). We have implemented our approach in the LTSmin model checking toolset and compare its performance with the A* implementation supported by ProM. We generated more than 4000 experiments (Petri net model and log trace combinations) by setting various parameters, and analysed performance and related these to structural properties. Our empirical study shows that the symbolic technique is in general better suited for computing alignments on large models than the A* approach. Our approach is better performing in cases where the size of the state-space tends to blow up. Based on our experiments we conclude that the techniques are complementary, since there is a significant number of cases where A* outperforms the symbolic technique and vice versa.

AB - Conformance checking is a branch of process mining that aims to assess to what degree a given set of log traces and a corresponding reference model conform to each other. The state-of-the-art approach in conformance checking is based on the concept of alignments. Alignments express the observed behaviour in terms of the reference model while minimizing the number of mismatches between the event data and the model. The currently known best algorithm for constructing alignments applies the A* shortest path algorithm for each trace of event data. In this work, we apply insights from the field of model checking to aid conformance checking. We investigate whether alignments can be computed efficiently via symbolic reachability with decision diagrams. We designed a symbolic algorithm for computing shortest-paths on graphs restricted to 0- and 1-cost edges (which is typical for alignments). We have implemented our approach in the LTSmin model checking toolset and compare its performance with the A* implementation supported by ProM. We generated more than 4000 experiments (Petri net model and log trace combinations) by setting various parameters, and analysed performance and related these to structural properties. Our empirical study shows that the symbolic technique is in general better suited for computing alignments on large models than the A* approach. Our approach is better performing in cases where the size of the state-space tends to blow up. Based on our experiments we conclude that the techniques are complementary, since there is a significant number of cases where A* outperforms the symbolic technique and vice versa.

KW - conformance checking

KW - process mining

KW - model checking

KW - symbolic reachability

KW - alignment

KW - algorithm

KW - graph search

U2 - 10.1109/ACSD.2018.00008

DO - 10.1109/ACSD.2018.00008

M3 - Chapter

SN - 978-1-5386-7013-2

SP - 50

EP - 59

BT - 2018 18th International Conference on Application of Concurrency to System Design

PB - IEEE

ER -

Bloemen V, van de Pol J, van der Aalst WMP. Symbolically Aligning Observed and Modelled Behaviour. In 2018 18th International Conference on Application of Concurrency to System Design : Proceedings. IEEE. 2018. p. 50-59 https://doi.org/10.1109/ACSD.2018.00008