Strong Connectivity and Shortest Paths for Checking Models

Vincent Bloemen

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    437 Downloads (Pure)


    We study directed graphs and focus on algorithms for two classical graph problems; the decomposition of a graph into Strongly Connected Components (SCCs), and the Single-Source Shortest Path problem. In particular, we concentrate on the development of new graph search algorithms for checking models, i.e. techniques that allow a user to analyse a system and verify whether particular properties are maintained. Our contributions advance the performance of state-of-the-art techniques for model checking and conformance checking. Moreover, we additionally pursue new directions to broaden the horizons of both fields.

    We developed a multi-core algorithm for on-the-fly SCC decomposition that scales effectively on many-core systems. In its construction, we additionally developed an iterable concurrent union-find structure that may be used in other applications.

    We considered SCCs in the domain of model checking and showed that our SCC decomposition algorithm can be applied to outperform the state-of-the-art techniques. Additionally, we explored how more general automata could be model checked by providing techniques to achieve this.

    We studied the shortest path problem in the context of conformance checking, in particular for the computation of alignments. By exploiting characteristic choices for the cost function, we compute alignments via an algorithm based on symbolic reachability. We also consider an alternative cost function and show how this leads to a new data structure and algorithm.

    Finally, we studied new problems for Parametric Timed Automata (PTAs), which extend timed automata with unknown constant values, or parameters. We developed algorithms to synthesize parameter values for the best- and worst-case behaviour. For instance, computing all parameter valuations such that a target location is reached in minimal- or maximal time.
    Original languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • University of Twente
    • van de Pol, Jaco , Supervisor
    • van der Aalst, Wil M.P., Co-Supervisor, External person
    Award date10 Jul 2019
    Place of PublicationEnschede
    Print ISBNs978-90-365-4786-4
    Publication statusPublished - 10 Jul 2019


    • Algorithms
    • Model checking
    • Graph theory
    • Process mining
    • Automata


    Dive into the research topics of 'Strong Connectivity and Shortest Paths for Checking Models'. Together they form a unique fingerprint.
    • Maximizing Synchronization for Aligning Observed and Modelled Behaviour

      Bloemen, V., van Zelst, S. J., van der Aalst, W. M. P., van Dongen, B. F. & van de Pol, J., 2018, Business Process Management: 16th International Conference, BPM 2018, Sydney, NSW, Australia, September 9–14, 2018, Proceedings. Weske, M., Montali, M., vom Brocke, J. & Weber, I. (eds.). Cham: Springer, Vol. 11080. p. 233-249 17 p.

      Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

      Open Access
      13 Citations (Scopus)
      231 Downloads (Pure)
    • Parallel Model Checking Algorithms for Linear-Time Temporal Logic

      Barnat, J., Bloemen, V., Duret-Lutz, A., Laarman, A., Petrucci, L., van de Pol, J. & Renault, E., 2018, Handbook of Parallel Constraint Reasoning. Hamadi, Y. & Sais, L. (eds.). Cham: Springer, p. 457-507 51 p.

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

      Open Access
      18 Citations (Scopus)
      372 Downloads (Pure)
    • Symbolically Aligning Observed and Modelled Behaviour

      Bloemen, V., van de Pol, J. & van der Aalst, W. M. P., 2018, 2018 18th International Conference on Application of Concurrency to System Design : Proceedings. IEEE, p. 50-59 10 p.

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

      Open Access
      13 Citations (Scopus)
      185 Downloads (Pure)

    Cite this