Dynamic Linear Time Temporal Logic

Publisher Website
Google Scholar
Abstract
A simple extension of the propositional temporal logic of lineartime is proposed. The extension consists of strengthening the untiloperator by indexing it with the regular programs of propositionaldynamic logic (PDL). It is shown that DLTL, the resulting logic, isexpressively equivalent to S1S, the monadic second-order theoryof omega-sequences. In fact a sublogic of DLTL which correspondsto propositional dynamic logic with a linear time semantics isalready as expressive as S1S. We pin down in an obvious mannerthe sublogic of DLTL which correponds to the first order fragmentof S1S. We show that DLTL has an exponential time decisionprocedure. We also obtain an axiomatization of DLTL. Finally,we point to some natural extensions of the approach presentedhere for bringing together propositional dynamic and temporallogics in a linear time setting.

This publication has 0 references indexed in Scilit: