Name
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, Gastin and Kuske (2003) [10]) and remains in PSPACE for all classical local temporal logics even if the dependence alphabet is part of the input, Gastin and Kuske (2007) [8]. 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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1016/j.ic.2009.12.003 | CONCUR |
Keywords | Field | DocType |
satisfiability,temporal logic | Discrete mathematics,Computer science,Upper and lower bounds,Concurrency,Boolean satisfiability problem,PSPACE,Temporal logic,Systems architecture,Monadic predicate calculus,Monad (functional programming) | Journal |
Volume | Issue | ISSN |
208 | 7 | Information and Computation |
ISBN | Citations | PageRank |
3-540-28309-9 | 8 | 0.53 |
References | Authors | |
15 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paul Gastin | 1 | 1165 | 75.66 |
| Dietrich Kuske | 2 | 485 | 47.93 |