@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.}
}

{"_id":"ZLgR7Fm86653Efiye","bibbaseid":"hirsch-hustadt-translatingpltlintows1sapplicationdescription-2001","author_short":["Hirsch, B.","Hustadt, U."],"bibdata":{"bibtype":"incollection","type":"incollection","author":[{"propositions":[],"lastnames":["Hirsch"],"firstnames":["Benjamin"],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]}],"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.","bibtex":"@INCOLLECTION{Hirsch+Hustadt@M4M2001,\n AUTHOR = {Hirsch, Benjamin and Hustadt, Ullrich},\n TITLE = {Translating PLTL into WS1S: Application Description},\n BOOKTITLE = {Methods for Modalities II},\n PUBLISHER = {University of Amsterdam},\n YEAR = {2001},\n URL = {Hirsch+Hustadt@M4M2001.pdf},\n ABSTRACT = {This paper introduces a technique for translating propositional linear\n time logic PLTL into the weak second-order logic of one successor\n WS1S. Using the MONA tool, a decision procedure for WS1S, we\n obtain a decision procedure for PLTL. We demonstrate the viability of\n this approach by an empirical comparison with STeP, SMV, and\n the Logics Workbench on a class of semi-randomly generated PLTL-formulae.}\n}\n","author_short":["Hirsch, B.","Hustadt, U."],"key":"Hirsch+Hustadt@M4M2001","id":"Hirsch+Hustadt@M4M2001","bibbaseid":"hirsch-hustadt-translatingpltlintows1sapplicationdescription-2001","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Hirsch+Hustadt@M4M2001.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"incollection","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["translating","pltl","ws1s","application","description","hirsch","hustadt"],"title":"Translating PLTL into WS1S: Application Description","year":2001}