Oct 11, 2016: Vincent Bloemen: Multi-core SCC-based LTL Model Checking and Ongoing Work on Checking ω-Automata

October 11, 2016Multi-core SCC-based LTL Model Checking and Ongoing Work on Checking ω-Automata
Room: HB 2BVincent Bloemen

In this talk I will talk about my work on multi-core SCC-based LTL model checking, to be presented at HVC. Additionally, I will talk about some related ongoing work, where I investigate different types of ω-automata and how these may be more suitable for (parallel) model checking, to be presented at the FM doctoral symposium.

HVC abstract:
We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel. To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.

FM doctoral symposium abstract:
Specifications for non-terminating reactive systems are described by ω-regular properties. Such properties can be translated in various types of automata, e.g. Büchi, Rabin, and Parity. A model checker can then check for language containment and determine whether the system meets the specification. Checking these automata becomes more complex when introducing probabilities and/or an adversary, e.g. the uncontrollable environment, to the automaton.

Parallel algorithms have become crucial for fully utilizing current hardware systems. With respect to model checking we therefore focus on designing scalable parallel algorithms for emptiness checking. This research focuses on designing and improving parallel graph searching algorithms for emptiness checking on various types of ω-automata. As a basis, we developed a scalable multi-core on-the-fly algorithm for the detection of strongly connected components (SCCs). Our aim is to contribute to the state-of-the-art techniques in parallel model checking, based on both theoretical complexity analysis and empirical studies on suitable benchmarks.