Designing tableau-like axiomatization for Propositional Linear Temporal Logic at home of Arthur Prior

Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. The paper suggests a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.