Mar 17, 2015: Alfons Laarman: Partial-Order Reduction for Multi-Core LTL Model Checking

March 17, 2015Partial-Order Reduction for Multi-Core LTL Model Checking
Room: HB 2AAlfons Laarman

In my PhD thesis, I developed several parallel model checking algorithms. One of the remaining open issues was their combination with partial-order reduction. To this end, a parallel solution had to be found for the so-called ignoring problem, which boils down to covering all cycles in a graph, also known as the Vertex Feedback Set. As this NP-compete problem has to be solved on-the-fly on a graph that is already exponentially sized in the input, we usually attack it via an approximation with depth-first search (DFS). Using similar techniques as developed in my thesis, we show how such a DFS solution can be parallelized efficiently. Because strict DFS order is P-complete, therefore likely not parallelizable, we focus on preserving enough of the search order to still detect all cycles, while at the allowing for enough parallelism to obtain good speedups on practical inputs.