Abstract:

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.

DOI:
Issue
Pages:
113-136
File:
shilov_3.pdf (241.68 KB)