Мы представляем формально-логический метод спецификации свойств мультиагентных систем реального времени, позволяющий в явном виде формализовать понятие действия агента, недетерминированный метод взаимодействия с внешней средой, механизм кооперации агентов, а также ограничения на время реакции системы. Предлагаемый метод расширяет возможности динамической логики PDL и логики альтернированного времени ATL, вводя новые конструкции для описания временных ограничений, предоставляя тем самым естественный формализм спецификации математической модели мультиагентной системы. Задача верификации системы по спецификации для предложенного формализма разрешима за полиномиальное время.