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

L'interface pour l'outil pttf

Tapez ou copiez le programme de transitions dans la zone de texte et appuyez sur le bouton Envoyer pour obtenir le graphe modèle. Voir pour plus d'informations sur l'outil pttf, sur la syntaxe du langage d'entrée, et essayez un exemple.

Tapez votre exemple pttf:

-p: le graphe modèle en format 'plain'
-c: le graphe modèle en format 'compact'
-g: le graphe modèle en format 'graphplace'
-f: le sous-graphe cyclique du graphe modèle en format 'graphplace'

Introduction à l'outil pttf

L'avantage des spécifications logiques temporelles vient du fait qu'on peut obtenir le graphe modèle des spécifications qui accepte toutes les séquences d'événements, d'actions ou d'états du système spécifié. Dans quelques conditions le graphe modèle peut être associé à un automate qui peut être utilisé dans l'implémentation du système.

Dans la conception d'une grande partie de systèmes comme systèmes distribués, systèmes en temps réel, systèmes séquentiels, on peut utiliser un ensemble restreint de formules logiques temporelles, appelées formules de transitions. Pour cette classe de formules on peut élaborer des algorithmes spécifiques que peuvent être plus efficaces que les algorithmes pour les formules logiques temporelles arbitraires. Nous avons proposés une méthode simple d'analyse de la satisfiabilité des programmes de transitions, constitués d'un ensemble de formules de transitions temporelles, par la résolution d'un système d'équations de points fixes. Cette méthode est mise à la base de l'algorithme d'analyse de la satisfiabilité utilisé par l'outil pttf. Pour plus d'informations sur les formules de transitions et sur l'algorithme d'analyse de la satisfiabilité utilisé par pttf voir: Ursu A. Une méthode d'analyse de la satisfiabilité des formules temporelles de transitions.

En utilisant l'outil pttf on peut utiliser les formules propositionnelles temporelles de transitions, qui sont une classe de formules propositionnelles temporelles logiques (PTL), pour spécifier et pour implémenter une classe large de systèmes, comme les systèmes distribués, les systèmes en temps réel et les systèmes séquentiels.
En lignes générales la conception des systèmes en utilisant pttf consiste en :

Si on écrit la spécification (S) et puis on effectue l'analyse de la satisfiabilité (SA) en utilisant pttf, on obtient le graphe modèle (SA) -> (MG), qui, en cas que la spécification (S) est satisfiable, peut être interprété comme un automate d'états fini (A). L'automate d'états fini peut être utilisé dans l'implémentation du système, dans l'élaboration du code (C). Cet outil produit le graphe modèle à partir des spécifications pttf via l'analyse de la satisfiabilité. (L'analyse de la satisfiabilité est effectuée en utilisant implicitement la condition d'unicité des variables propositionnelles).

Typiquement, on peut effectuer les conceptions suivantes en utilisant les spécifications pttf:

Un exemple

Soit le programme de transitions suivant avec la condition d'unicité des variables propositionnelles par défaut: 

 
~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)))
.
Si on vérifie ce programme de transitions avec pttf en utilisant l'option -p on obtient: 
%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

La présentation de notre outil pttf est inspirée de la présentation de l'outil ptl, de Geert Janssen, qui est un analyseur de tautologies/satisfiabilité des formules PTL, implémente un autre algorithme et qui est basé sur les diagrammes binaires de décision.
Retour à la page principale