反例に基づく抽象化の洗練
記号モデル検査と論理計算の技術

反例誘導抽象化改良（CEGAR ）は、記号モデル検査の手法である。[1] [2]また、様相論理のタブロー 計算アルゴリズムの効率を最適化するためにも適用されている。 [3]

コンピュータ支援によるプログラムの検証および解析において、計算モデルは多くの場合、状態から構成されます。しかし、小規模なプログラムのモデルであっても、膨大な数の状態を持つ場合があります。これは状態爆発問題として認識されています。[4] CEGARはこの問題に、状態をグループ化してモデルを簡素化する抽象化と、抽象化の精度を高めて元のモデルにより近づける改良という2つの段階で対処します。

プログラムの望ましい特性が抽象モデルにおいて満たされていない場合、反例が生成される。CEGARプロセスは、反例が偽物であるかどうか、つまり、反例が抽象化不足モデルにも当てはまるが、実際のプログラムには当てはまらないかどうかをチェックする。もしそうであれば、反例は抽象化の精度不足に起因すると結論付ける。そうでなければ、プロセスはプログラムにバグを発見する。反例が偽物であると判明した場合、洗練が実行される。[5]反復手順は、バグが発見されるか、抽象化が元のモデルと同等になるまで洗練された時点で終了する。

プログラム検証

抽象化

プログラムの正しさ、特に並行性のための時間の概念を含むプログラムの正しさを推論するために、状態遷移モデルが用いられる。特に、有限状態モデルは時相論理と併用することで自動検証に用いられる。[6]このように、抽象化の概念は2つのクリプキ構造間のマッピングに基づいている。具体的には、プログラムは制御フローオートマトン（CFA）を用いて記述することができる。[7]

クリプキ構造をと定義する。ここで M {\displaystyle M} ⟨ S 、 s 0 、 R 、 L ⟩ {\displaystyle \langle S,s_{0},R,L\rangle }

  • S {\displaystyle S} 有限の状態集合である。
  • s 0 {\displaystyle s_{0}} は、 の初期状態であり、 S {\displaystyle S}
  • R {\displaystyle R} は全遷移関係であり、
  • L {\displaystyle L} 各状態に、そこに成立する命題名のセットでラベルを付ける関数です。

の抽象化は によって定義され、はのすべての状態を の状態にマッピングする抽象化マッピングです。[5] M {\displaystyle M} ⟨ S α 、 s 0 α 、 R α 、 L α ⟩ {\displaystyle \langle S_{\alpha },s_{0}^{\alpha },R_{\alpha },L_{\alpha }\rangle } α {\displaystyle \alpha} S {\displaystyle S} S α {\displaystyle S_{\alpha}}

モデルの重要な特性を維持するために、抽象化マッピングは、元のモデルの初期状態を抽象モデルの対応する状態にマッピングします。また、抽象化マッピングは、2つの状態間の遷移関係が保持されることを保証します。 s 0 {\displaystyle s_{0}} s 0 α {\displaystyle s_{0}^{\alpha}}

モデル検査

各反復処理において、抽象モデルに対してモデル検査が実行される。例えば、境界付きモデル検査では命題式が生成され、SATソルバーによってブール充足可能性が検査される。[5]

洗練

反例が見つかった場合、それが偽例、つまりモデルの抽象化不足から生じた不正な例であるかどうかを検査します。偽例ではない反例はプログラムの誤りを反映しており、プログラム検証プロセスを終了させ、プログラムが誤りであると結論付けるのに十分な場合があります。改良プロセスの主な目的は、偽例を処理することです。抽象化の粒度を高めることで、偽例を排除します。

精緻化プロセスは、行き止まり状態と不良状態が同じ抽象状態に属していないことを保証する。行き止まり状態とは、出力遷移を持たない到達可能な状態であるのに対し、不良状態とは、反例を引き起こす遷移を持つ状態である。[2]

タブロー計算

様相論理はクリプキ意味論で解釈されることが多く、クリプキフレームはプログラム検証に関係する状態遷移システムの構造に似ているため、CEGAR技術は自動定理証明にも実装されています。[3]

参考文献

  1. ^ Clarke, Edmund ; Grumberg, Orna ; Jha, Somesh ; Lu, Yuan ; Veith, Helmut (2003年9月1日). 「反例に基づく記号モデル検査のための抽象化改良」 . Journal of the ACM . 50 (5): 752– 794. doi :10.1145/876638.876643.
  2. ^ ab Clarke, Edmund ; Grumberg, Orna ; Jha, Somesh ; Lu, Yuan ; Veith, Helmut (2000).反例に基づく抽象化の洗練化. 国際コンピュータ支援検証会議 CAV 2000: コンピュータ支援検証. コンピュータサイエンス講義ノート. 第1855巻. ベルリン、ハイデルベルク: Springer. pp.  154– 169. doi :10.1007/10722167_15. ISBN 978-3-540-45047-4。
  3. ^ ab Goré, Rajeev; Kikkert, Cormac (2021年9月6日). CEGAR-Tableaux: 様相節学習とSATによる様相充足可能性の向上. 分析的Tableauxと関連手法による自動推論: 第30回国際会議, TABLEAUX 2021, 英国バーミンガム. コンピュータサイエンス講義ノート. 第12842巻. シュプリンガー出版. pp.  74– 91. doi :10.1007/978-3-030-86059-2_5. ISBN 978-3-030-86059-2。
  4. ^ Valmari, Antti (1998).状態爆発問題. ペトリネット上級講座, ACPN 1996. コンピュータサイエンス講義ノート. 第1491巻. ベルリン, ハイデルベルク: Springer. pp.  429– 528. doi :10.1007/978-3-642-35746-6_1. ISBN 978-3-540-49442-3. 2023年12月27日閲覧。
  5. ^ abc Clarke, Edmund ; Klieber, William; Nováček, Miloš; Zuliani, Paolo (2011).モデル検査と状態爆発問題. LASERソフトウェア工学サマースクール: LASER 2011. コンピュータサイエンス講義ノート. 第7682巻. pp.  1– 30. doi :10.1007/978-3-642-35746-6_1. ISBN 978-3-642-35746-6. 2023年12月27日閲覧。
  6. ^ クラーク, エドマンド; ブラウン, マイケル C. ;エマーソン, E. アレン; シストラ, AP 「有限状態システムの自動検証における時相論理の利用」並行システムの論理とモデルNATO ASI 第13巻 ベルリン、ハイデルベルク: シュプリンガーdoi : 10.1007/978-3-642-82453-1_1 . ISBN 978-3-642-82453-1。
  7. ^ ハイドゥ、アコス;ミッケイ、ゾルタン（2019年11月11日）。 「CEGAR ベースのモデル チェックの効率的な戦略」。自動推論ジャーナル。64 (4)。 Springer Nature: 1051–1091 . doi : 10.1007/s10817-019-09535-x。
「https://en.wikipedia.org/w/index.php?title=Counterexample-guided_abstraction_refinement&oldid=1298051770」から取得