M. K. Valiev
On verification of dynamic properties of multi-agent systems
We consider the problem of verifying dynamic (temporal) properties
for multi-agent systems (MA-systems) consisting of interacting
program agents with intellectual components. Such systems
represent one of the most actively developing areas in the modern
software engineering and artificial intelligence, and became
especially popular with development of Internet technologies.
In the model of the MA-systems which we consider, states of agents
are described by sets of facts (analogues of local relational
databases), the intellectual components are described by logical
programs with updates of the states, and interaction of agents is
performed through mailboxes. The model follows lines of MA-
systems with the IMPACT architecture introduced by V.S.
Subrahmanian et al., but is conceptually simpler and
moreconvenient for the theoretical investigation.
We define deterministic, nondeterministic and asynchronous
versions of operational semantics for the MA-systems. It is clear that
verifying some rather simple dynamic properties is undecidable for
the general logic programs which can work with infinite state
spaces. To exclude this we introduce some natural restrictions on
intellectual components of agents which make all systems we
consider, finite-state.
The dynamical properties of the deterministic MA-systems are
natural to describe in some variants of the first-order logic of linear
time, and the properties of nondeterministic and asynchronous
MA-systems in the first-order logic of branching time or in the first-
order temporal mu-calculus.
It is clear that verifying these properties for the (finite-state) MA-
systems is decidable. But in the most general case of verifying
formulas of mu-calculus on nonground nondeterministic or
asynchronous MA-systems the time complexity is very high:
nondeterministic double exponential. Our main results are
connected with establishing some tight bounds on complexity of the
problem for restricted classes of MA-systems. In some cases of these
restrictins we have deterministic or nondeterministic polynomial time
complexity, in other - completeness in EXPTIME, and so on.
(with M. I. Dekhtyar, A. Ja. Dikovsky)