• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

1999 年度 研究成果報告書概要

エージェントの分散制約充足に基づく計算機システムの検証および診断

研究課題

研究課題/領域番号 09650444
研究種目

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 システム工学
研究機関北海道工業大学

研究代表者

栗原 正仁  北海道工業大学, 工学部, 教授 (50133707)

研究期間 (年度) 1997 – 1999
キーワードエージェント / 分散制約充足 / 検証 / 診断 / 書換え系 / 停止性 / 完備化
研究概要

本研究はエージェントの分散制約充足という基盤技術に関して、その推論技術の組織化に取り組み,それを計算機システムの検証および診断に応用してその有効性を実証したもので,その成果は大きく4つに分けられる.
1.ソフトウェアの検証問題として書換え系で記述されたプログラムの停止性検証を取り上げ,それを制約充足問題として定式化し,これを解くためのエージェントの組織を二分決定グラフで構造化する手段を開発した.その技術的ポイントは,各エージェントが単に独立して動作するのではなく,二分決定グラフにより組織化されることにより,情報交換による情報共有が可能となり,システムが効率的に動作することにある.
2.ハードウェアの故障診断のための推論を念頭に,機能仕様が等式で記述されることに着目して,等式系に対する完備化と呼ばれる推論技術による制約充足判定のマルチエージェント化を行った.マルチエージェントにより複数の半順序を平行して扱うことを可能にし,さらに独自の真偽維持システムを通して強調することにより,効率的な制約充足判定を実現する手段を実現した.
3.書換え型プログラムを扱うエージェントが自己認識に基づいて動作をするような構造的枠組みとして,書換え型言語へ自己反映計算メカニズムを導入した.ベースレベルとメタレベルのメッセージ交換プロトコルを設計し,エージェントの動作を公理論的に定義し,その操作的意味により計算のモデルを定義した.
4.エージェントの分散制約充足系および故障診断系を実装するためのソフトウェアアーキテクチャとしてJava言語に基づく分散オブジェクト指向アーキテクチャを提示し,ネットワーク実環境上で実際にシステムを構築し、典型的なテスト問題により評価して結果が期待されていたように良好であることを示した.

  • 研究成果

    (21件)

すべて その他

すべて 文献書誌 (21件)

  • [文献書誌] 近藤久: "二分決定グラフを用いた項書換え系の停止性検証システム"人口知能学会誌. 13. 822-834 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 沼澤政信: "条件付項書換え系に基づく言語におけるメタ計算"情報処理学会論文誌. 39. 3035-3043 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Kurihara: "Completion for multiple reduction orderings"Journal of Automated Reasoning. 23. 25-42 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Kurihara: "Heuristics and experiments on BDD representation of Boolean functions for expert systems in software verification"Lecture Notes in Artificial Intelligence. 1747. 353-364 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] H. Kondo: "Design and heuristics for BDD-based automated termination verification system for rule-based programs"Proc. Australian Joint Conf. On Artificial Intell.. 11. 85-96 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Noto: "A method for proving termination of functional programs"Proc. 1997 Int. Tech. Conf. On Circuits/Systems, Computers and Communications. 1. 47-50 (1997)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Numazawa: "Reflection in conditional REPS"Proc. 1997 Int. Tech. Conf. On Circuits/Systems, Computers and Communications. 1. 319-322 (1997)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Noto: "Termination verification of equational programs"Proc. 1998 Int. Tech. Conf. On Circuits/Systems, Computers and Communications. 1. 359-362 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Numazawa: "Reflective systems in rewriting language"Proc. 1998 Int. Tech. Conf. On Circuits/Systems, Computers and Communications. 1. 1161-1164 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Kurihara: "Binary decision diagrams for mechanical verification of precedence-based termination of rewrite rules"Proc. 5th Pacific Rim Intern. Conf. On Artificial Intelligence. 1. 7-12 (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] H.Kondo and M.Kurihara: "Termination verification system for term rewriting systems using binary decision diagram"Journal of Artificial Intelligence Society of Japan. 13. 822-834 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Numazawa, M.Kurihara and A. Ohuchi: "Meta-computation in a conditional term rewriting system-based language"Transaction of Information Processing Society of Japan. 39. 3035-3043 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Kurihara and H.Kondo: "Completion of multiple reduction orderings"Journal of Automated Reasoning. 23. 25-42 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Noto, M. Kurihara and A. Ohuchi: "A method for proving termination of functional programs"Proc. 1997 Intern. Technical Conf. On Circuits/Systems, Computers and Communications. 47-50 (l997)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Numazawa M.Kurihara and A. Ohuchi: "Reflection in conditional REPS"Proc. 1997 Intern. Technical Conf. On Circuits/Systems, Computers and Communications. 319-322 (1997)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Noto and M. Kurihara: "Termination verification of equational programs"Proc. 1998 Intern. Technical Conf. On Circuits/Systems, Computers and Communications. 359-362 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Numazawa, M. Kurihara and A. Ohuchi: "Reflective systems in rewriting language"Proc. 1998 Intern. Technical Conf. On Circuits/Systems, Computers and Communications. 1161-1164 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Numazawa, M. Kurihara and A. Ohuchi: "Reflective agents for conditional rewriting"Proc. 11th Australian Joint Conf. On Artificial Intelligence. 85-96 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Kurihara and H. Kondo: "Binary decision diagrams for mechanical verification of precedence-based termination of rewrite rules"Proc. 5th Pacific Rim Intern. Conf. On Artificial Intelligence. 7-12 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] H. Kondo and M. Kurihara: "Design and heuristics for BDD-based automated termination verification system for rule-based programs"Proc. 1999 IEEE Intern. Conf. On Systems, Man and Cybernetics. 5. 738-743 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M. Kurihara and H. Kondo: "Heuristics and experiments on BDD representation of Boolean functions for expert systems in software verification domains"Proc. 12th Australian Joint Conf. On Artificial Intelligence, Lecture Notes in Artificial Intelligence. 1747. 353-364 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より

URL: 

公開日: 2001-10-23  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi