MOBILE AGENT SYSTEM SPECIFICATION USING THE TEMPORAL LOGIC OF ACTIONS

摘要

We propose an approach to formal specification of mobile agent systems using the temporal logic of actions. We consider specification of communication, dynamic creation, and mobility of agents. Agents can change location and communication capabilities. The model used is similar to dynamic input/output automata, but a mobile agent system is completely described in a logic, which consists of a formally defined language and a set of proof rules, allowing rigorous specification and verification of the system. The approach is explained with help of the same travel agent system example that has been employed to illustrate the dynamic input/output automata model.