Open AccessDynamic Linear Time Temporal Logic
Author(s) -
Jesper G. Henriksen,
P. S. Thiagarajan
Publication year - 1997
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v4i8.18798
Subject(s) - linear temporal logic , mathematics , interval temporal logic , zeroth order logic , extension (predicate logic) , temporal logic , propositional variable , fragment (logic) , dynamic logic (digital electronics) , discrete mathematics , linear logic , semantics (computer science) , intermediate logic , algorithm , computer science , theoretical computer science , multimodal logic , programming language , description logic , physics , transistor , voltage , quantum mechanics
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.