[] = toujoursQuestions linéaire logique temporelle (LTL)
O = suivant
! = Négation
<> = éventuellement
Vous vous demandez est-il [] <> est que équivaut à un peu []?
Également difficile de comprendre comment distribuer la logique temporelle.
[] [] (un OU! B)
! <>
[] ([] a ==> <> b)
Je vais utiliser les notations suivantes (a et b!):
F = éventuellement
G = toujours
X = suivant
U = jusqu'à
Dans mon cours model-checking, nous avons défini LTL la manière suivante:
LTL: p | φ ∩ ψ | ¬φ | Xφ | φ U ψ
Avec F étant un sucre syntaxique pour:
F (futur)
Fφ = True U φ
et G:
G (global)
Gφ = ¬F¬φ
Avec cela, votre question est:
Est-il vrai que: Gφ?= GFφ
GFφ < => G (True U φ)
Sachant que:
φ P ⊧ U ψ < => existe i> = 0: P _ (> = i) ⊧ ψ ET forall 0 < = j < i: P_ (< = j) ⊧ φ
De là, on voit clairement que GFφ indique qu'il doit toujours être tru e que φ sera toujours vérifié après un certain temps i, et avant cela (j avant i) True doit être vérifié (trivial).
Mais Gφ indique que φ doit toujours être vrai, "de maintenant à toujours" et non "de i à pour toujours".
Gp indique que, en tout temps p détient. GFp indique que, à tout moment, p tiendra le coup. Ainsi, alors que la trace infinie pppppp ... satisfait à la fois du cahier des charges, une trace infinie de la forme p (! P) (! P!) P (! P) p ... ne satisfait que GFp mais pas Gp. Pour être clair, ces deux exemples de traces doivent contenir un nombre infini d'emplacements, où p est valide. Mais dans le cas de GFp, et seulement dans ce cas, il est acceptable qu'il y ait des emplacements entre les deux, où p ne tient pas.
Donc, la réponse courte à la question ci-dessus par contre-exemple est: non, ces deux spécifications ne sont pas les mêmes.