正式な方法：[] <> TLAの無限頻繁に（常に最終的に）

Question

TLAでの私の理解から、最終的なアクション（<>）は次の状態で吃音を起こさせません。それで、無限に頻繁に（[] <>）の次の状態変数が吃音を許されないということですか？

天気予報の例を挙げると、最終的には何年にもわたることがあります（私たちはいつ起きるかわかりません）、雨が降るでしょう。

私の理解は無限に向いていますか？私が間違っているなら、私を訂正してください。

ありがとうございます。

Answer 1

プロパティ[]<> ϕが

• は無限の長さを有し、
• が<>[] ¬ϕを検証していないこと痕跡によって検証され、すなわちϕが決定的false永遠

になるまでの時間にポイントがありません

[] ϕを満たす無限のトレースも[]<> ϕ前者は後者よりも強いからです。逆の場合は必ずしもそうではありません。

[]<> it_rains_todayのような文は次のトレースによって満たされることになる。

• トレースS。T.それは永遠に毎日絶え間なく毎日雨が降ります
• トレースs.t.毎日雨が降ります。
• 痕跡s.t.すべての永遠に1年に1度、10年ごとに雨が降る。
• Aトレースs。規則性の任意の種類で発生するこのようなイベントのための要件が​​ないことを永遠

注意のために、それはこのような言葉を例にちょうど容易になり、すべての10万年一日雨が降ります。 唯一の必要条件は、が存在しないことを示しています。その後、いつまでも完全に雨に降ります。