2

LTL（線形時相論理）に慣れていない場合は、この質問をスキップしてください。もちろん、LTLはプログラミングにとって非常に重要です。これは、プログラムの検証に使用するモデル検査システムの中核であるためです。

これらの命題記号とその意味を考えると...
Gp-常に
PFp-時々P

次のステートメントはどういう意味ですか？

GFGp = ?  
FGFp = ?

私はLTLを取り巻くロジックに苦労しており、上記のステートメントに頭を悩ませることはできません。助けてくれてありがとう！

4

4 に答える 4

4

最初にいくつかの用語：

論理式は、すべての組み合わせ規則を満たすロジック内の文です。通常、これには、原子命題が論理式であるという帰納的定義があり、次のようになります。

論理式（WFF）と（通常の論理記号を置き換える...）&&、||、！、および=>の組み合わせも論理式です。これはすべて標準のFOLです。（線形）時相論理は、さらにいくつかの組み合わせの可能性を追加するため、F（WFF）、G（WFF）、およびX（WFF）自体が論理式になります。

F（WFF）自体が論理式である可能性があるため、論理式としてF（F（WFF）を使用でき、G（F（F（WFF））やその他の多くの奇妙に見える集合体も使用できます。しかし、それらはどういう意味ですか？

個人的に言えば、複雑な式の命題のセットの観点から考えると便利だと思います。ここで、Gは命題のセットを指し、Fは単一の命題を呼び出します。おっしゃるように、現在のノードがある場合、Fpはそのノードの少なくとも1つのサクセサで発生することを意味し、Gpはpが現在のノードのすべてのサクセサで発生することを意味します。

したがって、GFpすべての状態（この状態の後）には、発生する少なくとも1つの継承状態があると言いpます。したがって、p各操作の後に（将来的に）発生することが保証されます。

FGp後継者の完全なセットがである少なくとも1つの状態（この状態の後に）があることを意味しpます。ですから、プロセスの中には、それがpずっと続くというポイントがあります。

さらに進んでいくFGFpと、その後にいくつかのポイントがあると言いGFpます。繰り返しになりますが、すべての操作から（少なくとも1回）続くGFp必要があります。したがって、全体としては、将来的にすべてから取得することを意味します（もちろん、これは、その時点からすべてのものであることを意味する可能性があります。最後の状態）。pppp

GFGpすべての州の後継者が。であることを意味しFGpます。これは、パス内のすべてのポイントに、子孫がすべてp'sである継承状態があることを意味すると思います（パス全体が' sであるため、これは近いように見えますが、同じではありませんp）。

まだ混乱していますか？私は。

于 2011-04-08T23:49:31.743 に答える
2

私はそれを思います

Fpは、Pが最終的に保持されることを意味します（後続のパスのどこか）。

したがって、GFpは、パスのどこにいても「立っている」場合でも、pが後続のパスのどこかに保持されることを意味する必要があります。または、言い換えると、pはパスの無限の後続の場所に保持されます。

FGpは、後続のパス上に、それ以降常にpが立つ場所があることを意味する必要があります。

よくわかりませんが、GFGpはFGpと同じように証明できます

FGFpはGFpと同じです。

于 2011-04-08T22:37:24.960 に答える
1

理解しやすくするために、別の表記法を使用します。

G = globally = [] = always
F = finally = <> = eventually

したがって、[] <> pは、pが無限に頻繁に発生することを意味します。つまり、発生が停止することはありません。たとえば、** p ******* p ***** p *** p *** .. ..

式<>[]pは、シーケンス内にある場所があり、その後はpのみが中断されずに発生することを意味します。例：*** ppppp .. ..

ここで、<> [] <> pは、最終的にpが無限に頻繁に発生することを意味します。これは、pが無限に頻繁に発生するのとまったく同じです。つまり、<。[] <> p = []<>pです。

同様に、[] <> [] pは、任意の時点から、最終的には常にpであることを意味します。しかし、これは最終的にはpであると正確に言っているので、[] <> [] p = <>[]pです。

于 2013-07-14T01:30:17.907 に答える
0

GFGp = FGpの例：すべての犬は最終的に天国に行き、いつの日か永遠にそこにとどまります

FGFp = GFp：遅かれ早かれ、すべての犬は天国に行きます（そして、彼らが地球上で降りる/生まれ変わるなどの場合、彼らは再び避難所に行きます）。

于 2017-04-21T03:10:53.250 に答える