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

本研究着眼于智能体的分布式约束满足，发展了智能体的推理能力组织，并将其应用于计算机系统的验证和诊断问题。研究结果总结如下四项1.通过将重写系统的终止性验证描述为约束满足问题来研究软件验证。提出了一种利用二叉决策图(BDDS)结构来组织智能体的方法。关键在于，代理不是独立工作，而是通过有组织的BDD结构交换信息来共享信息，从而使整个系统更加高效。方程系统的完备化过程是一种基于等式规范的约束满足推理机制，其在硬件故障诊断中的应用受到多智能体的重视。这使得代理可以并行处理部分订单，并通过独特的真值维护系统进行协作，从而实现高效的约束满足过程。在重写语言中引入了反射计算机制，作为重写程序的认知主体的结构框架。设计了基本级和元级之间的消息交换协议。给出了智能体行为的公理定义，其操作语义定义了智能体的计算模型。在基于Java的分布式面向对象软件体系结构中，实现了实际网络环境下基于代理的分布式约束满足系统和故障诊断系统。通过对典型试题的评价，表明了该方法的有效性。

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.