Research on Temporal Spatial Logic on the Verification of Behaviors of Multi-Agents Considering Security

本研究旨在为分布式环境下多Agent的行为提供一个理论模型，并在此模型的基础上进行软件的高可靠性开发，主要研究成果如下：1.开发了ad-hoc网络中的多Agent控制系统、分布式资源访问控制系统和会议日程安排系统等原型系统，并对这些原型系统进行了仿真评估。我们还讨论了采用核查人员的问题。因此，我们提出了适用于环境变化的机制，即使代理的行为或意图相互冲突，也不会给网络带来沉重的负担。2.我们扩展了时间空间推理系统RCC（Region Connection Calculus），提出了一种能够以合作的方式处理空间属性和语义属性的模型。我们已经探索了完整的算法，区域的位置关系可以从区域的语义属性中推导出来，反之亦然。我们还实现了将数字数据表示的图形或图像转换为符号表达式的系统，以及检查表达式的等价性的系统。3.利用进程代数对胡子博弈进行了建模，并证明了进程代数可以形式化地表示进程与状态转移之间的相互作用。我们还使用模型检查器验证了一个回合的终止和整个游戏的终止。这种方法可以应用于代理通信中的传播周期性和终止性等问题。

This research aims at the development of software high reliability by providing a theoretical model for the multiagents' behaviors in the distributed environment, and developing the software based on this model.The research results are as follows :1.We have developed prototypes : multiagent controlling system in ad-hoc networks, access controlling system to distributed resources, and arrangement system for meeting schedules, and evaluated these systems by simulation. We have also discussed the introduction of verifying agents. As the result, we have proposed the mechanism that is applicable to environmental change without loading the heavy burden onto the network even if behaviors or intentions of agents conflict with each other.2.We have extended RCC(Region Connection Calculus), one of temporal spatial reasoning systems, and proposed the model which can handle the spatial property and semantical property in a corporate manner. We have explored the complete algorithm in that positional relations of regions can be derived from semantical properties that hold on regions and vise versa. We have also implemented the system which transforms the numerical data representing figure or image to the symbolic expression, and the system for checking the equivalence of the expressions. As the result, we have extended the field of applications of temporal spatial reasoning systems.3.We have modelled a beard game using process algebra, and showed that we can represent formally the interaction between processes and state transitions. We have also verified the termination of one turn and that of the entire game using a model checker. This approach can be applied to such problems as periodicity and termination of the propagation in agent communications.