An Axiomatization of PCTL*

Abstract

A sound and complete axiomatization for a computation tree logic with past operators, PCTL* is given. The logic extends the standard branching time logic CTL* of R-generable models via the use of past time operators and semantics based on a finite linear past leading back from any point in any fullpath. This is a conservative extension of CTL*. The past operators allow us to avoid use of any unusual rules of inference such as the ugly automata-motivated AA rule which was part of a recent complete axiomatization for CTL*.

Full Paper

Postscript of Accepted version of 19/05/2005

Status

Accepted Information and Control, 9/05/2005.

Bibtex

@article{Rey:pctlstar,
    author="M. Reynolds",
    title="An Axiomatization of PCTL*",
journal="Information and Control",
    year="accepted 2005",
pages="?--?"
}