Since 2014
Dynamic Linear Time Temporal Logic
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Dynamic Linear Time Temporal Logic
|
|
| Creator |
Henriksen, Jesper G.
Thiagarajan, P. S. |
|
| Description |
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.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-08
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18798
10.7146/brics.v4i8.18798 |
|
| Source |
BRICS Report Series; No 8 (1997): RS-08 Dynamic Linear Time Temporal Logic
BRICS Report Series; Nr. 8 (1997): RS-08 Dynamic Linear Time Temporal Logic 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18798/16443
|
|