Вероятностные мультиагентные системы: семантика и верификация

Рассматриваются системы взаимодействующих вероятностных интеллектуальных агентов. У них имеются два источника неопределенности: неопределенность времени передачи сообщений в каналах связи и неопределенность в результатах выполняемых действий. Показано, как таким системам за полиномиальное время могут быть сопоставлены конечные цепи Маркова. Это позволяет перенести известные результаты о верификации динамических свойств конечных цепей Маркова на вероятностные мультиагентные системы.