CTL* Model Checking on a Shared-Memory Architecture

In this paper we present a parallel algorithm for CTL* model checking on a virtual shared-memory high-performance parallel machine architecture. The algorithm is automata-driven and follows a games approach where one player wins if the automaton is empty while the other player wins if the automaton is nonempty. We show how this game can be played in parallel using a dynamic load balancing technique to divide the work across the processors. The practicality and effective speedup of the algorithm is illustrated by performance graphs.