• Home
• Publications
• Software
• • CEX2
  • TSPASS

TSPASS

TSPASS is a fair automated theorem prover for monodic first-order temporal logic with expanding domain semantics and propositional linear-time temporal logic. Its implementation is based on the first-order theorem prover SPASS.

In addition to the theorem prover a preprocessing tool "fotl-translate" has been developed, which transforms input formulae into the normal form that the prover expects. The preprocessor and the prover are linked together by a shell script. An example file which describes the input syntax can be found here.

The theoretical foundations of TSPASS are described in Fair Derivations in Monodic Temporal Reasoning and in Implementing a Fair Monodic Temporal Logic Prover.

As an additional feature, TSPASS can fully-automatically construct models for satisfiable PLTL formulae. The theoretical background behind this feature can be found in Resolution-Based Model Construction for PLTL.

Download

The TSPASS system (i.e. the prover itself and the translation tool) is released under the terms and conditions of the GNU General Public Licence v3 (or later).

The latest release of the "fotl-translate" tool is version 0.16, and the latest version of "tspass" is 0.94.

The TSPASS source code can be compiled under x86 Linux systems. The source code and x86 binaries can be downloaded by using the links given below. The binaries were compiled under Fedora 13.

tspass-source-0.95-0.17.tar.gz
tspass-binaries-0.95-0.17.tar.gz

Changes

For "TSPASS":

• 0.94 -> 0.95:
  • Fixed a bug which can occur during the constant-flooding of non-monadic step clauses.
• 0.93 -> 0.94:
  • Disable the cycle elimination in reduced models as it can lead to incorrect results.
• 0.92 -> 0.93:
  • Ensure that all the required orderings are considered for the model construction procedure.
  • Fixed a crash which can occur when logical loop condition tests are enabled.
• 0.91 -> 0.92:
  • Performance improvements in the model construction implementation.
  • New reduction steps implemented that reduce the constructed model by discarding symbol renamings.
• 0.90 -> 0.91:
  • Ensure that subsumption between terminating loop search and non-terminating loop search clauses is not allowed.
  • Model construction for propositional temporal problems added.

For "fotl-translate":

• 0.16 -> 0.17:
  • Fixed a bug in the handling of non-monadic and non-ground eventuality literals.
• 0.15 -> 0.16:
  • Modified the parser so that it accepts formulae of the form and([F]), or([F]).
• 0.14 -> 0.15:
  • Possibility added to reduce propositional temporal problems to single-eventuality problems.
• 0.13 -> 0.14:
  • Fixed a bug related to the renaming of 'eventuality' formulae.
• 0.12 -> 0.13:
  • Fixed a bug related to 'equivalence' formulae.
• 0.11 -> 0.12:
  • Fixed a bug in the computation of the negation normal form, which is related to 'implication' formulae.
• 0.10 -> 0.11:
  • Fixed bugs in the computation of the negation normal form, which are related to 'unless' and 'until' formulae.
  • Fixed memory leaks.