B. Hirsch and U. Hustadt (2001): Translating PLTL into WS1S: Application Description

B. Hirsch and U. Hustadt: ``Translating PLTL into WS1S: Application Description.''
Abstract, PostScript, Software: TRP.

This paper introduces a technique for translating propositional linear time logic PLTL into the weak second-order logic of one successor WS1S. Using the MONA tool, a decision procedure for WS1S, we obtain a decision procedure for PLTL. We demonstrate the viability of this approach by an empirical comparison with STeP, SMV, and the Logics Workbench on a class of semi-randomly generated PLTL-formulae.

The Prolog source for the translator can be downloaded here. [an error occurred while processing this directive]