Dynamic Linear Time Temporal Logic

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 omega-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.