Abstract:
A simple extension of the propositional temporal logic of
linear time is proposed. The extension consists of strengthening the until
operator by indexing it with the regular programs of propositional dynamic
logic (PDL). It is shown that DLTL, the resulting logic, is expressively
equivalent to S1S, the monadic second-order theory of 
-sequences. In
fact a sublogic of DLTL which corresponds to propositional dynamic logic with
a linear time semantics is already as expressive as S1S. We pin down in an
obvious manner the sublogic of DLTL which correponds to the first order
fragment of S1S. We show that DLTL has an exponential time decision
procedure. We also obtain an axiomatization of DLTL. Finally, we point to
some natural extensions of the approach presented here for bringing together
propositional dynamic and temporal logics in a linear time
setting
Available as PostScript, PDF, DVI.