Temporal Logics with Reference Pointers and Computation Tree Logics

Download Edit this record How to cite View on PhilPapers
Abstract
A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. 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.
Reprint years
2000
ISBN(s)
PhilPapers/Archive ID
GORTLW
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA
Modal Logic with Names.Gargov, George & Goranko, Valentin
[Omnibus Review].Goldblatt, Robert
Hybrid Languages.Blackburn, Patrick & Seligman, Jerry

View all 13 references / Add more references

Citations of this work BETA
Annotation Theories Over Finite Graphs.Gabbay, Dov M. & Szałas, Andrzej
Back From the Future.Masini, Andrea; Viganò, Luca & Volpe, Marco

Add more citations

Added to PP index
2013-12-01

Total views
66 ( #29,372 of 40,652 )

Recent downloads (6 months)
27 ( #20,685 of 40,652 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.