抽象モデル検査

コンピュータサイエンスと数学において、抽象化モデル検査は、モデルのみを開発するには実際の表現が複雑すぎるシステムに対するモデル検査の一形態です。そのため、設計は縮小された「抽象」バージョンへの一種の変換を受けます。

変数のセットは、値の変化に応じて可視と不可視に分割されます。実際の状態空間は、可視の変数の小さなセットにまとめられます。

実空間と抽象状態空間はガロア接続されています。つまり、抽象空間から要素を取り出して具体化し、具体化されたバージョンを抽象化すると、結果は元のものと等しくなります。一方、実空間から要素を取り出して抽象化し、抽象バージョンを具体化すると、最終結果は元のもののスーパーセットになります。

つまり、

${\displaystyle \eta}$( (抽象)) = 抽象 ( (実数)) 実数 ${\displaystyle \theta}$
${\displaystyle \theta}$${\displaystyle \eta}$${\displaystyle \supseteq}$

• Edmund M. Clarke、Orna Grumberg、David E. Long (1994)。「モデル検査と抽象化」。ACM Transactions on Programming Languages and Systems。16 ( 5): 1512–1542。CiteSeerX 10.1.1.79.3022。doi : 10.1145 / 186025.186051。S2CID 207884170  。