整数制約論理のための二分決定グラフの拡張データ構造とそれに対するアルゴリズムの提案

摘要

本稿では，ある整数制約論理の処理のためのデータ構造およびその上での論理演算に関する基本アルゴリズムを提案する．例えば，リアルタイムシステムの設計では，システムのイベントの発生などを時刻で表し，システムの仕様はイベント発生時刻が満たすべき制約からなる論理式として表現することができる．具体的に得られた設計仕様が要求仕様を満たすかどうかを形式的に検証するには，時刻を表す変数を含む論理式を処理し，要求仕様を満足するかどうかを検証する必要がある．本研究では，イベント発生時刻を整数変数で表現し，一つの論理項に最大2つの整数変数を含むような項からなる論理式を取り扱う．そのような論理式を表現するデータ構造を提案し，そのデータ構造に対する論理演算処理について述べる．これらの基本処理を組み合わせることにより，モデル検査アルゴリズムなどの検証アルゴリズムを実現することができる．