Решение автоматных уравнений для временных автоматов относительно параллельной композиции

Аннотация

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