T. Kapus (Slovenia)
Software Agents, Formal Methods, Temporal Logic of Actions, Dynamic Input/Output Automata.
We propose an approach to formal specification of mobile agent systems using the temporal logic of actions. We con sider 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 for mally 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.
Important Links:
Go Back
