Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces

Abstract

We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.