Model Checking CTL is Almost Always Inherently Sequential

Olaf Beyersdorff, Arne Meier, Martin Mundhenk +3

The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the…