A Multi-agent Framework Based on Communication and Concurrency

摘要

Multi-agent systems are receiving attention nowadays, as they can be applied in a variety of disciplines like industry, e-commerce, control systems, etc. As the areas of usage are more crucial the matter of assurance of correctness of programs is important. However, verification of these systems has received attention only very recently. Hitherto such systems have been programmed without a clearly defined formal semantics and with very little idea about formally expressed verifiable properties to be satisfied by such systems. In this paper a new multi-agent programming language, called ECCS is defined. Its operational semantics is defined and a model checking algorithm is described which verifies properties expressed in the logic ACTL.