Translating PLTL into WS1S: Application Description. Hirsch, B. & Hustadt, U. In Methods for Modalities II. University of Amsterdam, 2001.
Translating PLTL into WS1S: Application Description [pdf]Paper  abstract   bibtex   
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.
@INCOLLECTION{Hirsch+Hustadt@M4M2001,
 AUTHOR        = {Hirsch, Benjamin and Hustadt, Ullrich},
 TITLE         = {Translating PLTL into WS1S: Application Description},
 BOOKTITLE     = {Methods for Modalities II},
 PUBLISHER     = {University of Amsterdam},
 YEAR          = {2001},
 URL           = {Hirsch+Hustadt@M4M2001.pdf},
 ABSTRACT      = {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.}
}
Downloads: 0