Research On Agent Interactions Based On Pi-Calculus

With the rapid development of computer hardware and networking technology, application software becomes more and more complex. Consequently, an important research topic in software engineering is how to describe user requirements precisely, how to develop, manage complex software system and support software reusability effectively. Multi-Agent Systems (MAS) provides a new approach to the development of complex software; it is very suited to tackle the problems which have competitive solving methods, multiple view-points and various solvers. The main difference between MAS and traditional software system is that MAS are more autonomous, more reactive, more collaborative and more adaptive to dynamic environments. Because of these characteristics, the development of MAS is beyond the current technology; formal methods will play an important role in making MAS be ripe in theory so that they could be more applicative to real life.This paper presents a formal method for specification and quantitative analysis of agent interactions. The behaviors of agents are specified in Pi-Calculus; analyses of various properties of runtime transition processes of MAS, such as deadlock-free, are achieved using explicit representations of interaction processes and operational semantics of Pi-Calculus. By establishing a one-to-one correspondence between MAS transition process and a Markov chain, stochastic analysis techniques are applicable. Especially, stationary probability distribution is computed. The advantage of this approach is that qualitative specification and quantitative analysis of agent-interactions can be done uniformly in the same framework. On one side, by considering functional characteristics of different agents with different roles, formal specification can help us implement process logic of agents; one the other side, quantitative analysis of agent interaction help us make system more flexible and more reusable. Comparison of theoretical results and simulation results proves that this approach is reliable and applicable to real life systems.