-
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).
-
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).
-
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).