In the 1st NASA Workshop on Formal Approaches to Agent-Based System (FAABS), pages 48-62, April, 2000. Springer Verlag Lecture Notes in Artificial Intelligence 1871.
Our project examines the power of the following three formal methods in studying different agent applications: (1) Erdos is a knowledge-based environment for agent programming; it supports dynamic creation of agents, dynamic loading of programs, and migration. Erdos also supports automatic model checking using CTL. (2) Nepi2 is a programming language for agent systems, based on the pi-calculus. It extends the pi-calculus with data types and a facility for communication with the environment. (3) I/O automata is a mathematical framework extensively used for modeling and reasoning about systems with interacting components. We have extended the I/O automata formalism to account for issues that arise in agent systems, such as dynamic creation and destruction of agents, mobility, and naming. We model a simple e-commerce system using the three formalisms.