Local temporal logic is expressively complete for cograph dependence alphabets
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. (C) 2004 Elsevier Inc. All rights reserved.
temporal logics mazurkiewicz traces concurrency