PLTLmona (PLTL-to-MONA translator)

PLTLmona is a simple Prolog program that translates formulae of propositional linear-time logic into input files suitable for the MONA model checking tool and executes MONA on the resulting files.

You can download MONA from the homepage of the MONA project.

The translation morphism implemented in PLTLmona has been described and proved to be satisfiability preserving in Hirsch and Hustadt (2001). This paper also illustrates the viability of the approach by empirical comparions of PLTLmona with other decision procedures for propositional linear-time logic.

Below you find the source code for PLTLmona which includes instructions on how to use it.