Complexity of verification of nondeterministic probabilistic multiagent systems

Probabilistic systems of interacting nondeterministic intelligent agents are considered. The states of agents in such systems are probabilistic databases (of facts), and their actions are controlled by probabilistic logical programs. Besides, communication channels between agents are also probabilistic. It is shown how such systems can be transformed in poynomial time to equivalent finite Markov decision processes. This makes it possible to translate the known results on the verification of the dynamic properties of the finite Markov processes to the probabilistic multiagent systems of the considered type.