scholarly journals Propositional Dynamic Logic with Recursive Programs

Author(s):  
Christof Löding ◽  
Olivier Serre
2007 ◽  
Vol 73 (1-2) ◽  
pp. 51-69 ◽  
Author(s):  
Christof Löding ◽  
Carsten Lutz ◽  
Olivier Serre

1988 ◽  
Vol 21 (1) ◽  
pp. 419-426
Author(s):  
Tinko Tinchev ◽  
Dimiter Vakarelov

1997 ◽  
Vol 4 (8) ◽  
Author(s):  
Jesper G. Henriksen ◽  
P. S. Thiagarajan

A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.


Sign in / Sign up

Export Citation Format

Share Document