Logique modale (temporelle)

• A, B ::= … ½ SW.A ½ ST.A

• SW.A = quelque part (maintenant) il y a un emplacement satisfaisant A.

• ST.A = dans le futur (ici) il y a une “configuration” satisfaisant A.