Strong Connectivity and Shortest Paths for Checking Models

Vincent Bloemen

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

9 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 UTAcademic

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