Title :
More past glories [temporal logic]
Author_Institution :
Murdoch Univ., WA, Australia
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;
Conference_Titel :
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location :
Santa Barbara, CA, USA
Print_ISBN :
0-7695-0725-5
DOI :
10.1109/LICS.2000.855772
