Strong Connectivity and Shortest Paths for Checking Models

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.