Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor D
In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal...