Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Information and Computation Année : 2010

Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces

Résumé

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.

Domaines

Autre [cs.OH]

Dates et versions

hal-00779916 , version 1 (22-01-2013)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook X LinkedIn More