Translating PLTL into WS1S: Application Discription

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.

Authors:
Benjamin Hirsch, Ullrich Hustadt
Category:
Conference Paper
Year:
2001