More Past Glories

Abstract

We continue in the same vein as Lichtenstein, Pnueli and Zuck 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 rewritesand is shown to be a useful alternative to automata-based temporal reasoning. The use of the normal form axiomatization for CTL*, in providing a complete axiomatizationfor PCTL* (i.e. CTL* with past connectives) is sketched.

Full Paper

Is not available on-line due to IEEE copyright restrictions. It will appear in the proceedings of LICS'2000.

Status

To appear in LICS'2000.

Bibtex

@inproceedings{Rey:mpg,
author="M. Reynolds",
title="More Past Glories",
booktitle="LICS'2000",
publisher="IEEE",
year="to appear 2000",
}