# IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

# Logic in Computer Science (LICS 1995)

## Invited Paper: A Complete Proof Systems for QPTL (at LICS 1995)

Authors: Yonit Kesten Amir Pnueli

### Abstract

The paper presents an axiomatic system for \emm{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 for 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 performing equivalence transformations on this automata, formally justifying these transformations.

### BibTeX

  @InProceedings{KestenPnueli-ACompleteProofSyste,
author = 	 {Yonit Kesten and Amir Pnueli},
title = 	 {A Complete Proof Systems for QPTL},
booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
year =	 {1995},
month =	 {June},
pages =      {2--12},
location =   {San Diego, CA, USA},
note =       {Invited Talk},
publisher =	 {IEEE Computer Society Press}
}