The paper presents an axiomatic system for quantified propositional temporal logic (QPTL), which is propositional temporal logic equipped with quantification over propositions (Boolean variables). The advantages of this extended temporal logic is that its expressive power is strictly higher than that of the un-quantified version (PTL) and is equal to that of S1S, as well as that of &omega-automata. Another important application of QPTL is its use of formulating and verifying refinement relations between reactive systems. In fact, the completeness proof is based on the reduction of a QPTL formula into a Buchi automaton, and preforming equivaelnce tranformations on this automata, formally justifying these transformations as a bi-directional refinement.
Journal of Logic and Computation