• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

1999 Fiscal Year Final Research Report Summary

VERIFICATION AND DIAGNOSIS OF COMPUTER SYSTEMS BASED ON DISTRIBUTED CONSTRAINT SATISFACTION OF AGENTS

Research Project

Project/Area Number 09650444
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field System engineering
Research InstitutionHOKKAIDO INSTITUTE OF TECHNOLOGY

Principal Investigator

KURIHARA Masahito  HOKKAIDO INSTITUTE OF TECHNOLOGY, DEPARTMENT OF ELECTRICAL ENGINEERING, PROFESSOR, 工学部, 教授 (50133707)

Project Period (FY) 1997 – 1999
Keywordsagent / distributed constraint satisfaction / verification / diagnosis / rewrite system / termination / completion
Research Abstract

This research focuses distributed constraint satisfaction of agents, develops organization of agents for their reasoning ability, and applies it to verification and diagnosis problems of computer systems. The results are summarized by the following four items.
1. Verification of software is investigated by formulating termination verification of rewrite systems as constraint satisfaction problems. The method for solving these problems is developed which organizes the agents by using the structure of binary decision diagrams (BDDs). The point is that the agents do not work independently, but share the information by exchanging it through the organized BDD structure, thus making the overall system more efficient.
2. Completion procedures of equational systems, a reasoning mechanism for constraint satisfaction of equality-based specifications, are multi-agentified for its application to hardware fault diagnosis in mind. This allows the agents to handle the partial orders in parallel and cooperate via the unique truth maintenance system, leading to efficient constraint satisfaction procedures.
3. A reflective computation mechanism is introduced into the rewrite language as a structural framework of epistemic agents for rewrite programs. Message exchange protocols between base- and meta-levels are designed. Axiomatic definition of agents' behavior is developed, while its operational semantics defines the model of computation for agents.
4. Agent-based distributed constraint satisfaction systems and fault diagnosis systems on real network environments are implemented in Java-based distributed object-oriented software architecture. The evaluation by typical test problems shows its effectiveness as expected.

  • Research Products

    (21 results)

All Other

All Publications (21 results)

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

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

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

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 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)

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

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

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

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

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

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

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

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

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

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] 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)

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

URL: 

Published: 2001-10-23  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi