『モデル検査入門』

モデル検査

検証したいシステムを表すクリプキ構造$ M と、検証したい性質を表す様相論理式$ φ を作って、$ M が$ φ を満たすかをソフトウェア(モデル検査器(model checker))を使って調べる

様相論理式が仕様

モデル検査器