Complexity of Asynchronous Behavior of Multi-Agent Systems
by
Mars Valiev
Keldysh Institute of Applied Mathematics
Coauthors: Michael Dekhtyar (Tver State University), Alexander Dikovsky (Keldysh Institute of Applied Mathematics)

The aim of this paper is to study the verification complexity of behavior properties of asynchronous intelligent multi-agent (MA-) systems. The range of applications of MA-systems is very broad and extends from operating system interfaces, processing of satellite imaging data and WEB navigation to air traffic control, business process management and electronic commerce.

There are a lot of readings and definitions of intelligent agents and MA-systems. Earlier we considered the verification of behavior properties of synchronous MA-systems which basically conform to the so called IMPACT architecture introduced and described in detail in the book of V.Subrahmanian et al. Their behavior properties are expressed as the properties of trajectories (paths) of the state transition diagrams they induce. This allows to use the classical temporal logics: PLTL, CTL, CTL^*, \mu-calculus, their variants and first-order extensions as languages to describe the behavior properties of the MA-systems. The ``MA-BEHAVIOR" problem we considered, consists in verifying that a temporal logic formula holds on the tree of trajectories of a given MA-system.

Here we study the complexity of the ``MA-BEHAVIOR" problem for similar systems with asynchronous semantics of message passing. We establish some tight complexity bounds on this problem under some natural structural and semantic restrictions on agent programs and actions. These bounds vary from nondeterministic polynomial time to double exponential time.

Date received: March 19, 2003

Copyright © 2003 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Mathematical Conference Abstracts. Document # cajy-21.