問題タブ [model-checking]

私はちょうどこの質問を思いつきました。Logic in Computer Science の本に書かれているように、LTL と同等の重要なものの 1 つに Fp=TUp があります。T は制約がないことを意味します。

しかし、T を (p ではなく) に置き換えるとどうなるでしょうか? Fp=(not p)Up は成り立ちますか? この場合、実際にはいくつかの制約 (p ではない) を数式に入れましたが、その間 (p ではない) と p を一緒に満たすことができる状態はありません。そして、異なる LTL 式を p として試してみました。p が充足可能である限り、p を持つすべてのパスについて、Fp と (p ではなく)Up も満たさなければなりません。このように F を書き換えることができるということですか、それとも反例があるのでしょうか?

ispin でシステムをモデル化しましたが、LTL 式を使用してシステムを検証しようとすると、次のような到達不能エラーが見つかりました

私のLTL式は

私は CTL 演習を行っています。次の式が同等かどうかを確認しようとしています。しかし、私は正しいことをしているかどうかわかりません。

最初の式: 等価

2 番目の式: 等価

3 番目の式: 等価

そうですか？間違っている場合は、クリプキ モデルで考えられる反例の 1 つを教えていただけますか?

前もって感謝します。

次のコードには、呼び出し規約エラー (永久ループにつながる可能性があります) があり、それを検出できません。「Satabs」を使用してコードを検証しようとします。どのようなモデルがエラーを表面化させることができますか。次のモデルでは、segfault が発生します。VLENとTMAXを変えることで少し遊べます。

• Q1. 呼び出し規約エラーとは何ですか?
• Q2. エラーを見つけるために使用するのに最も適したモデルはどれですか?

2 つの LTL を比較して、一方が互いに矛盾する可能性があるかどうかを確認するにはどうすればよいですか? 階層的なステート マシンと、各ステートの動作を説明する LTL があるためです。ローカル LTL がグローバル LTL と矛盾する可能性があるかどうかを知る必要があります。「機能仕様と自動競合検出」という記事で、L(f) の交差 L(g) が空である場合、2 つの LTL プロパティ f と g が矛盾することを見ました。そして、これはまさに、プログラムとして f とプロパティとして ¬g を使用したモデル チェックの問題です。誰でもこれで私を助けることができますか？LTL f を SPIN/Promela のプログラムに変換するにはどうすればよいですか??

ありがとう。

iSpin (v. 1.1.4) の "Automata View" は、正確には何を示していますか? 1つのプロセスの制御フローの単なるグラフのようです。

システムの完全な状態空間を取得するにはどうすればよいですか?

たとえば、Ben-Ari: Spin Model Checker の原理では、図 4.1 が必要です。または概要では、図1が必要です。

現在、R のコマンドに基づくスクリプトを使用してpairs、特定のモデルの残差と残りの変数との関係を見つけています。この関係は、モデルの診断にとって重要な場合があります。現在関係をプロットしている方法の小さな例については、以下のコードを参照してください。

モデルに多くの変数 (たとえば ~10) がある場合、pairsプロットは非常に大きくなります。pairs残差との関係を示すプロットの一番下の行のみを見ているため、プロットを大幅に単純化できます。ペアプロットの一番下の行のみをプロットするコマンドなどを推奨できますか?

新しいプロット方法が、非常に広いプロットの代わりに残差分析にグリッドを使用できれば素晴らしいことです。

dput(gpa) からの出力

NuSMV で単純なバブル ソートを FSM としてプログラムしようとしていますが、大きな問題に直面しています。配列の 2 つの要素間でスワップを実行しようとすると、配列でスワップを実行できません。プログラムが停止します。誰でもこれを解決できますか？どうもありがとう。