Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 5, October 2002: pp. 701-745

Complete Proof System for QPTL

Yonit Kesten1 and Amir Pnueli2

1Ben-Gurion University, Beer-Sheva, Israel. E-mail: ykesten@bgumail.bgu.ac.il
2Weizmann Institute of Science, Rehovot, Israel. E-mail: amir@wisdom.weizmann.ac.il

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 unquantified version (PTL) and is equal to that of S1S, as well as that of [ohgr]-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 Büchi automaton, and performing equivalence transformations on this automaton, formally justifying these transformations as a bi-directional refinement.

Keywords: Axiomatic system; temporal logic; completeness; rigid variable; flexible variables; Büchi automata; refinement; history scheme; prophesy scheme

Table of Contents   Full-Text PDF (398 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement