P Gastin, M Mukund and K Narayan Kumar
Proc. MFCS '03, Springer LNCS 2747 (2003) 429-438.
© Springer-Verlag Berlin Heidelberg
To obtain an expressively complete linear-time temporal logic (LTL) over Mazurkiewicz traces that is computationally tractable, we need to intepret formulas locally, at individual events in a trace, rather than globally, at configurations. Such local logics necessarily require past modalities, in contrast to the classical setting of LTL over sequences. Earlier attempts at defining expressively complete local logics have used very general past modalities as well as filters (side-conditions) on future modalities that implicitly talk about the past. In this paper, we show that it is possible to use unfiltered future modalities in conjunction with a constant number of past formulas of a restricted form and still obtain a logic that is expressively complete over traces.
Keywords Temporal logics, Mazurkiewicz traces, concurrency