An axiomatization of PCTL* (Q2566222)

In this paper a sound and complete axiomatization for \(\text{PCTL}^*\) (computation tree logic with past operators) is given. This axiomatization is for the logic presented by \textit{F. Laroussinie} and \textit{Ph. Schnoebelen} [``Specification in \(\text{CTL}\) + past for verification in \(\text{CTL}\)'', Inf. Comput. 156, 236--263 (2000; Zbl 1046.68599)], an extension of \(R\)-generable \(\text{CTL}^*\) of total Kripke structures with evaluation points being at indexes along full paths with a finite linear past. The temporal operators used are the so-called ``non strict temporal operators'' of standard \(\text{PLTL}\) (propositional linear temporal logic based on the natural numbers model of time) and \(\text{CTL}^*\). The semantics is defined with respect to a fixed set of full paths which may not be limit-closed, that is, closed under putting together a full path from ever increasing prefixes of full paths. On the other hand, the ``separation theorem'' technique used by \textit{D. M. Gabbay} [``An irreflexivity lemma with applications to axiomatizations of conditions on tense frames'', in: Aspects of philosophical logic, Synth. Libr. 147, 67--89 (1981; Zbl 0519.03008)] for eliminating past-time operators is also applied to \(\text{PCTL}^*\). Thus for every \(\text{PCTL}^*\) formula there exists an equivalent \(\text{CTL}^*\) formula if evaluated at the start of a full path. As a consequence, decidability of \(\text{PCTL}^*\) follows directly from decidability of \(\text{CTL}^*\). Finally, it is a remarkable feature of this paper that it shows how the safety-liveness form and past operators can be used without recourse to automata machinery to give a complete axiomatization for \(\text{PCTL}^*\).