Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)

TL;DR

This paper establishes a polynomial-time equivalence between Linear Temporal Logic and propositional schemata, explores complexity implications, and reports initial experimental results and potential implementation improvements.

Contribution

It introduces a formal reduction showing LTL's equivalence to propositional schemata and analyzes the complexity and practical implications.

Findings

Polynomial-time reductions between LTL and schemata

Complexity analysis of the equivalence

Initial experimental results and implementation insights

Abstract

This paper relates the well-known Linear Temporal Logic with the logic of propositional schemata introduced by the authors. We prove that LTL is equivalent to a class of schemata in the sense that polynomial-time reductions exist from one logic to the other. Some consequences about complexity are given. We report about first experiments and the consequences about possible improvements in existing implementations are analyzed.