Мы представляем алгоритмы автоматической верификации распределенных систем реального времени по их формально-логической спецификации методом MASL. Предложенные алгоритмы основаны на так называемом принципе символьной верификации (symbolic model checking), как и соответствующие алгоритмы для логик ветвящегося времени CTL и альтернированного времени ATL. Алгоритмическая сложность решения задачи верификации для случая MASL с фиксированной внешней средой ограничена полиномом от длины спецификации и мощности множества состояний и действий системы. Для случая MASL с неопределенной внешней средой, задача верификации разрешима за полиномиальное время от размера модели, но имеют экспоненциальную сложность относительно структуры спецификации среды.