Abstract of Paper

Local LTL with past constants is expressively complete for Mazurkiewicz traces
by Paul Gastin and Madhavan Mukund and K. Narayan Kumar

Abstract:

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) that ``look 
sideways'' and talk of concurrent events. In this paper, we show that it 
is possible to use unfiltered future modalities in conjunction with past 
constants and still obtain a logic that is expressively complete over traces.