A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance

Abstrakt

Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly.

We use this feature to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.

Klíčová slova

• Propositional linear temporal logic (PLTL)
• Decision procedure
• Resolution
• Semantic guidance
• Benchmarks