spin - SPIN は現在、制約を表現するための CTL をサポートしていますか?

Question

しばらくグーグルで検索したところ、SPIN の CTL または CTL* モデル チェックを提案している論文がいくつか見つかりました。ただし、Promela のマニュアル ページによると、Promela モデルで CTL を表現する方法はありません。今はちょうど提案レベルですか？

Answer 1

数ヶ月前に使用したばかりですが、もう一度確認してください。彼らの最近のリリース ノートにざっと目を通してみると、ノーと言わざるを得ません。特定の研究プロジェクトにアクセスできない限り、LTL プロパティのチェックのみがサポートされます。