Skip to Main content Skip to Navigation
Journal articles

Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces

Abstract : We continue our study of the complexity of MSO-definable local temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In previous papers, we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed) and remains in PSPACE for all classical local temporal logics even if the dependence alphabet is part of the input. In this paper, we consider the uniform satisfiability problem for arbitrary MSO-definable local temporal logics. For this problem, we prove multi-exponential lower and upper bounds that depend on the number of alternations of set quantifiers present in the chosen MSO-modalities.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-00779916
Contributor : Stefan Haar <>
Submitted on : Tuesday, January 22, 2013 - 5:07:11 PM
Last modification on : Monday, February 15, 2021 - 10:39:46 AM

Links full text

Identifiers

Citation

Paul Gastin, Dietrich Kuske. Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Information and Computation, Elsevier, 2010, 208 (7), pp.797-816. ⟨10.1016/j.ic.2009.12.003⟩. ⟨hal-00779916⟩

Share

Metrics

Record views

201