問題タブ [uppaal]

正式な方法のバックグラウンドを持っていない人に、検索が時間的に制限されている場合に、シンボリック モデル チェックを使用して仕様を検証することと、具象モデル チェックを使用して同じことを行うことの違いを説明するために、誰かが少し言葉を費やしてもらえますか? UPPAAL で作成された SMC と Concrete MC の定義を参照しています。

特に、UPPAAL Java API を使用して時限オートマトンのネットワークに対するクエリを検証するプログラムを作成しました。クエリが検証された場合、UPPAAL は解析するシンボリック トレースを返します。検証されていない場合は別の何かを返します。検証に時間がかかりすぎる場合は、検証プロセスを停止し、メッセージを返し、検証する次のクエリに進むことにしました。これまでのところ、すべてが順調です。

最近、私は UPPAAL Stratego で遊んでいます。これは、検索を制限するために最大時間または探索の深さを選択する可能性をネイティブに提供します。ただし、このオプションは、Concrete Model Checking を使用して検証を実行する場合にのみ適用できます。

私の質問は、Java プログラムで行っているシンボリック検証プロセスの停止と、UPPAAL Stratego がネイティブで行っていることとに違いはありますか? どちらの場合も、答え (またはトレース) は得られませんが、探索の「信頼性」はどうですか?

2 つのオプションのうち、どちらが優れている (つまり、より完全である) でしょうか? シンボリック検証を停止するか、具体的な検証を停止しますか?

これまでの私の理解では、シンボリック モデル チェックでは、可能な状態は変数の間隔を使用して定義されますが、具象モデル チェックでは、変数は実際の値を想定しています。私の見解では、「完全性」の観点から、状態空間の探索は BFS または DFS アルゴリズムを使用して体系的に行われるため、しばらくしてから SMC を停止する方がより「完全」であり、BFS を使用する場合は「確実に」できると考えています。 N ステップ以内に何も悪いことが起こらないこと。しかし、繰り返しになりますが、モデル チェックの経験が豊富ではないため、完全に間違っている可能性があります。

また、戦略への参照を削除できれば、本当にありがたいです。

ありがとう！