文章基本信息

标题：Dynamic Linear Time Temporal Logic
本地全文：下载
作者：Jesper G. Henriksen ; P. S. Thiagarajan
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1997
卷号：4
期号：8
出版社：Aarhus University
摘要：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.