Logique modale (spatiale)

• A, B ::= true ½ (not A) ½ (A or B)

• ½ 0 ½ a[A] ½ (A | B) ½ (A -o B)

• Logique propositionnelle avec les modalités:

  • le processus est vide!
  • il y a un ambient nommé a où A est satisfait (et rien d’autre.)
  • le processus se décompose en une partie satisfaisant A et une partie satisfaisant B (i.e. produit tensoriel.)
  • mis en parallèle avec un « contexte » satisfaisant A, le résultat satisfait B.