TTM: A Tableau-based Theorem Prover for Temporal Logic PLTL

Description

TTM is a theorem prover for the Propositional Linear Temporal Logic called PLTL.

TTM allows you to test the satisfiability of any set of PLTL-formulas.

TTM is based on a one-pass tableau method for PLTL called the context-based tableau method.

TTM has been implemented in Haskell using the Glasgow Haskell Compiler.

TTM v1.0 is a cross-platform.

Documentation

Example of use

Show a satisfiable model of a PLTL formula

$ ./ttm -i examples/sat2.txt 
This is a model of Set:

State 0:{ a }
State 1:{ a, b }
State 2:{ a, b }
State 3:{ a, b, c }
Cycle starts at the state 3

View the generated tableau with XDot

$ ./ttm -i examples/sat2.txt -d -o result.dot
$ /path/to/xdot.py result.dot

Man page

NAME
TTM - manual page for TTM 1.0-2011-04-28
Synopsis
ttm options
Description
-i|--input <input file>
Input file to read
-o|--output <output file>
Output file to write the model
-d|--dot
Output the infered tableaux in in Graphviz's dot language.
Use xdot to view the generated tableaux : ./ttm --dot --input examples/sat-1.txt > xdot.dot; /path/to/xdot.py xdot.dot
-l|--limit <-1 .. 2^29-1>
Limit the depth of the generated tableaux for debugging purposes. Note: Negative numbers represent infinite depth
-r|--repeated
Disable optimization which detects and avoids repeated unsatisfiable branches
-v|--version
output version information and exit

Screenshot

Download

TTM
XDot - Linux Dot viewer

All the above TTM-setups include a collection of examples for easily first testing

Related Publications

Dual Systems of Tableaux and Sequents for PLTL

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas
The Journal of Logic and Algebraic Programming 78: 701–722, (2009)

[JLAP09.pdf] [BibTeX] [Electronic Edition]

A Cut-Free and Invariant-Free Sequent Calculus for PLTL

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F.Orejas
In J. Duparc and T.A. Henzinger (Eds.): Computer Science Logic : 21 International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, LNCS 4646, pp. 481–495, Springer-Verlag Berlin Heidelberg, 2007.

[csl07.pdf] [BibTeX] [Electronic Edition]

Systematic Semantic Tableaux for PLTL

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro
In VII Jornadas sobre Programación y Lenguajes, PROLE’2007, Zaragoza, Spain, September, 2007,
Revised Selected Paper in ENTCS 206, pp. 59-73, 2008

[prole07b.pdf] [BibTeX] [Electronic Edition]

Please send comments, bugs and requests concerning to TTM to paqui.lucio@ehu.es

This work has been partially supported by the Spanish Project TIN2007-66523 and the Basque Project LoRea GIU07/35.

Last Modified: May 21th, 2011