Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets

Abstract. Recently, local logics for Mazurkiewicz traces are of increasing interest. This is mainly due to the fact that the satisfiability problem has the same complexity as in the word case. If we focus on a purely local interpretation of formulae at vertices (or events) of a trace, then the satisfiability problem of linear temporal logics over traces turns out to be PSPACE–complete if the dependence alphabet is not part of the input. But now the difficult problem is to obtain expressive completeness results with respect to first order logic. The main result of the paper shows such an expressive completeness result, if the underlying dependence alphabet is a cograph, i.e., if all traces are series parallel posets. Moreover, we show that this is the best we can expect: If the dependence alphabet is not a cograph, then we cannot express all first order properties in our setting. Keywords Temporal logics, Mazurkiewicz traces, concurrency

• Type: Conference
• Year: 2001
• Where: LPAR
• Authors: Volker Diekert, Paul Gastin
• Keywords: Automated Reasoning, Dependence Alphabet, LPAR 2001, Mazurkiewicz Traces, Satisfiability Problem