1. Все взаимодействия между диспетчером и пилотом, авионикой и надзорным контролем, полученные на этапе формализации требований, были преобразованы в 358-состояний Марковский процесс принятия решений (MDP), который точно моделирует вероятностный таймированный автомат. Глобальный таймер использовал двадцатитактные циклы, где один тик равен полутора секундам, чтобы отразить реальные временные дедлайны (см. рисунок 1).
2. Составной MDP прошёл исследование в ширину, при котором достигнута сходимость за 23 итерации, выявив 946 вероятностных переходов. Уравнения Беллмана были решены методом итерации по значению для задач достижимости и ожидаемого вознаграждения, при этом остаточная ошибка снизилась ниже подтверждая числовую корректность для как пессимистических, так и оптимистических стратегий планирования.
3. Всего было оценено шестнадцать PTCTL-свойств. Любая стратегия планирования — как враждебная, так и кооперативная — приводит к неизбежному завершению миссии, поскольку безусловная достижимость метки завершения доказала, что
