1. tarball for two satisfiability checkers for propositional linear temporal logic PLTL written in Ocaml.
   This prover implements two tableau-based methods: tree and graph.
   The tree method builds a rooted tree with ancestor cycles and passes up information about unfulfilled eventualities from the bottom up. It is based upon a method outlined by Stefan Schwendimann. It is a "one-pass" method in that it identifies unfulfilled eventualities without making any further passes of the tree that is built. The method is suboptimal since its worst case behaviour requires double-exponential time wrt the size of the input formula(e).
   The graph method also builds a rooted tree in a depth first left to right manner, but allows cross branch edges from one branch to a previous branch as well as ancestor cycles. It checks eventualities "on the fly", and has worst case behaviour that is exponential wrt the size of the input formula(e).
2. tarball for a graph-based multipass satisfiability checker propositional linear temporal logic PLTL written in Ocaml.
   This is an implementation of Wolper's method. It builds a cyclic graph and then makes multiple passes of the graph pruning inconsistent nodes and nodes that contain unfulfilled eventualities. Its worst case behaviour is exponential wrt the size of the input formula(e).
3. tarball for a BDD-based satisfiability and validity checker for propositional linear temporal logic PLTL written in C and using the BuDDy package.
   This prover implements the "finite property method" directly by creating the set of all CPL-consistent subsets of the Fischer-Ladner closure of the given formula and using a greatest fixpoint approach to delete sets and edges between them using the semantics of PLTL directly. Its worst case behaviour is exponential wrt the size of the input formula(e).