Strong Connectivity and Shortest Paths for Checking Models

Vincent Bloemen

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    88 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

    Fingerprint

    Model checking
    Decomposition
    Cost functions
    Directed graphs
    Data structures

    Keywords

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

    Cite this

    Bloemen, Vincent . / Strong Connectivity and Shortest Paths for Checking Models. Enschede, 2019. 264 p.
    @phdthesis{ebdae062220040deba24a496f8bc1360,
    title = "Strong Connectivity and Shortest Paths for Checking Models",
    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.",
    keywords = "Algorithms, Model checking, Graph theory, Process mining, Automata",
    author = "Vincent Bloemen",
    year = "2019",
    month = "7",
    day = "10",
    doi = "10.3990/1.9789036547864",
    language = "English",
    isbn = "978-90-365-4786-4",
    series = "DSI Ph.D. Thesis Series",
    number = "19-010",
    school = "University of Twente",

    }

    Bloemen, V 2019, 'Strong Connectivity and Shortest Paths for Checking Models', Doctor of Philosophy, University of Twente, Enschede. https://doi.org/10.3990/1.9789036547864

    Strong Connectivity and Shortest Paths for Checking Models. / Bloemen, Vincent .

    Enschede, 2019. 264 p.

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    TY - THES

    T1 - Strong Connectivity and Shortest Paths for Checking Models

    AU - Bloemen, Vincent

    PY - 2019/7/10

    Y1 - 2019/7/10

    N2 - 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.

    AB - 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.

    KW - Algorithms

    KW - Model checking

    KW - Graph theory

    KW - Process mining

    KW - Automata

    U2 - 10.3990/1.9789036547864

    DO - 10.3990/1.9789036547864

    M3 - PhD Thesis - Research UT, graduation UT

    SN - 978-90-365-4786-4

    T3 - DSI Ph.D. Thesis Series

    CY - Enschede

    ER -

    Bloemen V. Strong Connectivity and Shortest Paths for Checking Models. Enschede, 2019. 264 p. (DSI Ph.D. Thesis Series; 19-010). (IPA Dissertation Series; 2019-07). https://doi.org/10.3990/1.9789036547864