Dynamic linear time temporal logic

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. It is shown that DLTL, the resulting logic, is expressively equivalent to 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 expressively complete. We show that DLTL has an exponential time decision procedure and admits a finitary axiomatization. We also point to a natural extension of the approach presented here to a distributed setting.