Knowledge Dynamics and Behavioural Equivalencesin Multi-Agent Systems

We define a process calculus to describe multi-agent systems with timeouts for communication and mobility able to handle knowledge. The knowledge of an agent is represented as sets of trees whose nodes carry information; it is used to decide the interactions with other agents. The evolution of the system with exchanges of knowledge between agents is presented by the operational semantics, capturing the concurrent executions by a multiset of actions in a labelled transition system. Several results concerning the relationship between the agents and their knowledge are presented. We introduce and study some specific behavioural equivalences in multi-agent systems, including a knowledge equivalence able to distinguish two systems based on the interaction of the agents with their local knowledge.

Cloud manufacturing service composition and formal verification based on extended process calculus

Cloud manufacturing is an emerging service-oriented model to solve existing problems in manufacturing. This study proposes a process calculus–based approach to formally model cloud manufacturing service composition that is composed of description model, interaction scenario model, and composition process formal model, in which the semantics of process calculus to describe the quality of service (QoS) information of service composition is extended, and an intelligent service composition method is put forward based on the extended process calculus. Then, a platform architecture for implementing the proposed approach is addressed. The integrated development environment for the platform is set up with selection of free software tools. Thus, a prototype of the platform is developed. Finally, automated guided vehicle processing service composition and the open integrated manufacturing system service composition are taken as examples to illustrate the application of the proposed service composition method. The main attributes of the formal models for the application cases are verified. Case study results show that the proposed service composition and formal verification method based on the extended process calculus is feasible. Compared with other approaches for service composition, the proposed intelligent service composition method meets the most requirements for service composition.