DocumentCode
2221959
Title
More past glories [temporal logic]
Author
Reynolds, Mark
Author_Institution
Murdoch Univ., WA, Australia
fYear
2000
fDate
2000
Firstpage
229
Lastpage
240
Abstract
We continue in the same vein as O. Lichtenstein et al. (1985) in "The Glory of the Past", demonstrating the advantages of including past-time operators in using temporal logic in computer science. A normal form for temporal formulas, based on a simple combination of past formulas, is arrived at via syntactic rewrites and is shown to be a useful alternative to automata based temporal reasoning. The use of the normal form in providing a complete axiomatization for PCTL* (i.e. CTL* with past connectives) is sketched.
Keywords
automata theory; programming language semantics; rewriting systems; set theory; temporal logic; temporal reasoning; PCTL*; automata based temporal reasoning; complete axiomatization; computer science; normal form; past connectives; past formulas; past-time operators; syntactic rewrites; temporal formulas; temporal logic; Automata; Computer science; Logic; Machinery; Safety; Veins;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location
Santa Barbara, CA, USA
ISSN
1043-6871
Print_ISBN
0-7695-0725-5
Type
conf
DOI
10.1109/LICS.2000.855772
Filename
855772
Link To Document