これは非常に学術的な質問であることは承知していますが、ここの誰かが答えを得るのを手伝ってくれることを望んでいました.
LTS と FLTL を使用する同時実行クラスを受講しています。私たちの課題の 1 つで、「プログレス プロパティとして表現できない、FLTL 式として表現された liveness プロパティの例を挙げてください。」明確にするために、この質問に対する答えは望んでいません。
私の問題は、私が常に 2 を 1 と考えていたことです:) したがって、質問に答えるためには、progress プロパティと liveness プロパティの違いを知る必要があります。
どんな助けでも大歓迎です:)
liveness プロパティは、それを定義するときに、将来のある時点でプログラムがプログラムの特定の部分を実行することです。FSP では、ほとんどの活性プロパティを進捗プロパティとして定義できますが、割り当てでは、活性プロパティを FLTL として表現する例を考え出す必要がありますが、進捗プロパティとしては実行できません。
FLTL 式と FSP の進行状況プロパティの定義を参照して、それらがどのように異なるかを確認し、FSP 進行状況プロパティで何らかの制限が発生して 1 つとして表現できない例を考え出す必要があります。
さらに、私はそれについて少し読んだだけで、FSP の進行状況プロパティでは、アクション「入力」が発生したときに他のアクションが発生する可能性があるなど、「緩い」活性プロパティを記述することはできないようですが、最終的に「終了」アクションが発生します。これはプログレスプロパティとして記述できません.「入る」が起こる、「出る」が起こるなどの詳細しか記述できず、公平性の仮定の下では両方とも無限に頻繁に発生するため、FLTLでは可能です. [](enter -> <>exit) と言いますが、これは常に「enter」が発生すると、最終的に「exit」が発生することを意味します。これが、FSP と FLTL の形式化における進歩の大きな違いです。