Handling Periodic Properties: Deductive Verification for Quantified Temporal Logic Specifications

We present a deductive verification technique for the specifications written in terms of quantified propositional linear-time temporal logic (QPTL). The system extends previous natural deduction constructions for the propositional linear-time temporal logic. Our result expands the applicability of the natural deduction based verification in the temporal setting to more sophisticated specifications due to the expressive power of QPTL, which is equivalent to Buchi Automata. In particular, the paper introduces a novel formal framework to verify specifications of a larger set of useful periodic properties that are particularly important to maintain during different cycles of software integration. Moreover, the novel elegant and succinct natural deduction based verification method enables tracing the dependency of the verified properties on the assumptions of the underlying model and brings prospects for automation.