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)