Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle.

Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.