抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
正規モデル検査は,その構成が適切なアルファベット上の有限単語として表現できる無限状態システムの検証のための確立された技術である。それは,初期構成の集合が規則的であり,その遷移関係が長さ保存変換器によって捉えられるシステムに適用される。安全特性を検証するために,規則的モデル検査が,反復的に,到達可能構成のますます大きな規則的集合を認識し,それらが不安全構成を含むかどうかをチェックする。この手順はしばしば終了しないので,加速,抽象化および拡大技法を開発し,到達可能構成の集合の規則的スーパーセットを計算した。本論文では,相補的アプローチを開発した。下から到達可能な構成のセットに近づく代わりに,全ての構成のセットで開始し,ますます小さな規則的スーパーセットを計算した。到達可能構成のセットは,システムのすべての誘導不変量の交差点に等しい。交差点は一般に非正規であるので,b結合不変量を導入し,ほとんどのbクラスを用いてCNF形式で表現できるものとして定義した。著者らは,あらゆるb≧0に対して,すべてのb結合誘導不変量の交差が規則的であり,それを認識するオートマトンを構築する方法を示した。著者らは,このオートマトンがいくつかの不安全構成を受け入れるかどうかを決定する複雑性を研究した。問題は,b≧0に対してEXPSPACE,b=1に対してPSPACE完全であることを示した。最後に,多数のベンチマークの安全特性を証明するのに大まかななければならないかを研究した。【JST・京大機械翻訳】
