Logic in Computer Science (LICS 2000)

Paper: More Past Glories (at LICS 2000)

Authors: Mark Reynolds

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 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.

BibTeX

  @InProceedings{Reynolds-MorePastGlories,
    author = 	 {Mark Reynolds},
    title = 	 {More Past Glories},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {229--240},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }