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

点击翻译按钮获取中文摘要

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.