Temporal Logics with Reference Pointers and Computation Tree Logics
作者:
Valentin Goranko,
期刊:
Journal of Applied Non-Classical Logics
(Taylor Available online 2000)
卷期:
Volume 10,
issue 3-4
页码: 221-242
ISSN:1166-3081
年代: 2000
DOI:10.1080/11663081.2000.10510998
出版商: Taylor & Francis Group
关键词: Computation tree logics;temporal logics;reference pointers;axiomatic system;completeness
数据来源: Taylor
摘要:
A complete axiomatic system CTLrpis introduced for a temporal logic for finitely branching ω+-trees in a language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTLrp. In particular, that yields a complete axiomatization for the translations of all valid CTL*-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium for reasoning about branching time.
点击下载:
PDF (1019KB)
返 回