CTL* Model Checking on a Shared-Memory Architecture

Cornelia P. Inggs and Howard Barringer


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.