Anton Wijs: The Hitchhiking Algorithm for Massively Parallel LTL Model Checking

Event Details

Efficient algorithms have been developed to model check LTL formulae on-the-fly, such as the well-known Nested Depth-First Search, which uses a depth-first search (DFS) strategy. However, in some settings, such as when considering distributed model checking on a cluster, or many-core model checking using a Graphics Processing Unit (GPU), Breadth-First Search (BFS) is a more natural choice, at least for basic reachability analysis. LTL verification, however, requires the detection of `accepting’ cycles, and BFS is not very suitable to detect these on-the-fly. I will propose a new algorithm, the Hitchhiking algorithm, for model checking LTL formulae with a BFS-like strategy. It builds on the existing Piggyback algorithm from 2012, but whereas that algorithm is incomplete, the Hitchhiking algorithm is complete.