Strong Connectivity and Shortest Paths for Checking Models

Vincent Bloemen

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    163 Downloads (Pure)

    Abstract

    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
    Supervisors/Advisors
    • van de Pol, Jaco , Supervisor
    • van der Aalst, Wil M.P., Co-Supervisor
    Award date10 Jul 2019
    Place of PublicationEnschede
    Print ISBNs978-90-365-4786-4
    Electronic ISBNs978-90-365-4786-4
    DOIs
    Publication statusPublished - 10 Jul 2019

    Keywords

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

    Fingerprint Dive into the research topics of 'Strong Connectivity and Shortest Paths for Checking Models'. Together they form a unique fingerprint.

  • Cite this