Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces

Paul Gastin 1, 2 Dietrich Kuske 3
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2010, 208 (7), pp.797-816. 〈10.1016/j.ic.2009.12.003〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00779916
Contributeur : Stefan Haar <>
Soumis le : mardi 22 janvier 2013 - 17:07:11
Dernière modification le : mardi 24 avril 2018 - 01:16:11

Lien texte intégral

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

124