Propositional Temporal Transition Formulas (PTTF) Satisfiability Checker
(Un outil d'analyse de la satisfiabilité des Formules Propositionnelles Temporelles de Transition)

The interface to pttf tool

Type or copy your transition program into the text area and press the Start button to receive the model graph in one of the desired formats. See more information about pttf tool, about pttfinput language syntax, as well as try an example.

Type your pttf-example:

-p: model graph written in plain format
-c: model graph written in compact format
-g: model graph written in 'graphplace'-format
-f: only the cyclic part of the model graph written in 'graphplace'-format

Introduction to pttf tool

The advantage of the temporal logic specifications is based on the fact that it is possible to obtain the model graph of the specifications which accepts all the sequences of the events, actions or states of the specified system. Under some conditions the model graph can be associated with an automaton which can be used in the implementation of the system.

In the design of a large class of systems like distributed, real time and sequential systems, one can use a restricted set of temporal logic formulas, called transition formulas. For this class of formulas specific algorithms can be designed which are expected to be more efficient than the algorithms for the arbitrary temporal formulas. A simple satisfiability analysis method for transitions programs, composed of a set of temporal transition formulas, by solving a system of fixpoint equations has been proposed and is used in the implementation of the pttf tool. More information about the transition formulas and the satisfiability analysis algorithm used by pttf you can find in: Ursu A. A satisfiability analysis method for the temporal transition formulas.

With pttf tool it is possible to use propositional temporal transition formulas, which are a subset of the linear time propositional temporal logic (PTL) formulas, to specify and implement a large class of systems, such as distributed, real time and sequential systems.
Basically the pttf based design consists of:

If you write the specification (S) and then perform the satisfiability analysis (SA) using pttf, you obtain a model graph (SA) -> (MG), which, in case the specification (S) is satisfiable, can be interpreted as a finite state automaton (A). The finite state automaton can be used in the implementation of the system, that is in the code (C) generation. This tool produces the model graph of the specifications from the satisfiability analysis. (Satisfiability analysis is carried out using the default single propositional variable condition).

Typically, the following designs can be carried out using pttf:

An example

Given the Transition Program with the default single propositional variable condition: 

~Pr U (e1 \/ e2 \/ e5 \/ e3)

[]((e3 \/ e4 \/ e5) -> @(~Pr U (e1 \/ e3)))

[]((e2 \/ e4 \/ e3) -> @(~Pr U (e1 \/ e4)))

[]((e3) -> @(~Pr U (e1 \/ e5)))

[]((e2 \/ e1) -> @(~Pr U (e1 \/ e4 \/ e3)))
.
If we check this transition program with pttf using option -p we get: 
%pttf -p Example.pttf

*** PTTF Version 1.3 1999 Anatol Ursu, Ecole polytechnique, France ***

The initial condition:
   {e3 e5 e2 e1}

The Transitions:
 Antecedent: 1
   {e1 e2}
 Consequent: 1
   {e3 e4 e1}
 Antecedent: 2
   {e3}
 Consequent: 2
   {e5 e1}
 Antecedent: 3
   {e3 e4 e2}
 Consequent: 3
   {e4 e1}
 Antecedent: 4
   {e5 e4 e3}
 Consequent: 4
   {e3 e1}


The nodes of the Model Graph:
{{e3 e1 e4}
 {e4 e1}
 {e3 e1}
 {e1}
 {e3 e5 e2 e1}
}

The Model Graph in plain format:
The node 1:
 {e3 e5 e2 e1}
  The outgoing edge:
    e1
  The destination node :
    {e3 e1 e4}
  The outgoing edge:
    e2
  The destination node :
    {e4 e1}
  The outgoing edge:
    e5
  The destination node :
    {e3 e1}
  The outgoing edge:
    e3
  The destination node :
    {e1}

The node 2:
 {e1}
  The outgoing edge:
    e1
  The destination node :
    {e3 e1 e4}

The node 3:
 {e3 e1}
  The outgoing edge:
    e1
  The destination node :
    {e3 e1 e4}
  The outgoing edge:
    e3
  The destination node :
    {e1}

The node 4:
 {e4 e1}
  The outgoing edge:
    e1
  The destination node :
    {e3 e1 e4}
  The outgoing edge:
    e4
  The destination node :
    {e1}

The node 5:
 {e3 e1 e4}
  The outgoing edge:
    e1
  The destination node :
    {e3 e1 e4}
  The outgoing edge:
    e4
  The destination node :
    {e1}
  The outgoing edge:
    e3
  The destination node :
    {e1}

Satisfiability analysis:
   True

For the presentation of our pttf tool we have been inspired by the presentation of the Geert Janssen's tool ptl, which is a PTL tautology/satisfiability checker and uses a different algorithm based on binary decision diagrams.
Back to Top