Dynamic linear time temporal logic

Henriksen, Jesper G. ; Thiagarajan, P. S. (1999) Dynamic linear time temporal logic Annals of Pure and Applied Logic, 96 (1-3). pp. 187-207. ISSN 0168-0072

PDF - Author Version

Official URL: http://www.sciencedirect.com/science/article/pii/S...

Related URL: http://dx.doi.org/10.1016/S0168-0072(98)00039-6


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.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
Keywords:Linear Time Temporal Logic; Dynamic Logic; ω-Automata; Expressive Completeness; Axiomatizations
ID Code:50498
Deposited On:25 Jul 2011 11:44
Last Modified:18 May 2016 04:46

Repository Staff Only: item control page