動的環境におけるエージェント知識の効率的モデル検査法
スポンサーリンク
概要
- 論文の詳細を見る
有限状態の遷移で記述される動的環境下で一連の事象が起きた後に,その環境にいるエージェントがどのような知識を持つかという問題を,van der Meydenは様相論理式のモデル検査の形で定式化した.彼は,完全な記憶を持つ分散同期システムにおいて,状態系列γが与えられたとき,その最終時点で知識様相命題が真か偽かの判定(モデル検査)を,γの長さ(つまり状態変化の回数)∣γ∣についてO(∣γ∣)の時間計算量で計算する方法を示した.しがし,∣γ∣の係数は状態の数∣W∣に依存し,本論文で示すように最悪の場合∣W∣に関しては指数オーダ以上で増大する.本論文では,上と同様の設定において,「知らない」ということが表せないように制限された知識命題論理式(単調知識命題論理式)に限定した場合に,時間計算量が∣γ∣に関して線形時間であると同時に∣W∣に関して多項式時間であるモデル検査が可能であることを示す.
- 一般社団法人情報処理学会の論文
- 1999-11-15
著者
関連論文
- 信念変更と論理
- アブダクション
- 2. 演繹データベースの形式的意味論 (演繹データベース)
- 動的環境におけるエージェント知識の効率的モデル検査法
- モナドに基づく代数仕様の書換え
- マルチエージェント環境における遡行的信念推定アルゴリズム
- トランザクション論理におけるプログラム変換