Abstract

This paper introduces a technique for translating porpositional 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 viablilty of this approach by an empirical comparision with STeP, SMV, and the Logics WorkBench on a class of semi-randomly generated PLTL formulae.