Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces

Issue title: Half a Century of Inspirational Research: Honoring the Scientific Influence of Antoni Mazurkiewicz

Article type: Research Article

Authors: Gastin, Paul | Kuske, Dietrich

Affiliations: LSV, ENS Cachan & CNRS, France. E-mail: [email protected] | Institut für Informatik, Universität Leipzig, Germany. E-mail: [email protected]

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.

Journal: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 169-197, 2007