On complexity of verification of nondeterministic probabilistic multiagent systems

Probabilistic systems of interacting nondeterministic intelligent agents are considered. States of the agents in these systems are some probabilistic databases, and the activity of the agents is controlled by some probabilistic logic programs. Moreover, communication channels between agents are also probabilistic. We show how such systems can be polynomially transformed to finite state Markov decision processes. This allows one to transfer the known results on verifying temporal properties of the finite state Markov processes to the probabilistic multi-agent systems of considered type.