An axiomatization of PCTL*

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. Furthermore, the valid formulas of CTL* are also valid in PCTL*. The past operators allow us to avoid use of any unusual rules of inference such as the ugly automata-motivated AA rule which is part of the existing complete axiomatization for CTL*.