Abstract:
We present here a linear time temporal logic which
simultaneously extends LTL, the propositional temporal logic of linear time,
along two dimensions. Firstly, the until operator is strengthened by indexing
it with the regular programs of propositional dynamic logic (PDL). Secondly,
the core formulas of the logic are decorated with names of sequential agents
drawn from fixed finite set. The resulting logic has a natural semantics in
terms of the runs of a distributed program consisting of a finite set of
sequential programs that communicate by performing common actions together.
We show that our logic, denoted 
, admits an
exponential time decision procedure. We also show that
is expressively equivalent to the so called regular
product languages. Roughly speaking, this class of languages is obtained by
starting with synchronized products of (
-)regular languages and
closing under boolean operations. We also sketch how the behaviours captured
by our temporal logic fit into the framework of labelled partial orders known
as Mazurkiewicz traces
Available as PostScript, PDF, DVI.