On the verification of strictly deterministic behavior of timed finite state machines

Конечные автоматы широко применяются в качестве математических моделей при решении многочисленных задач в области программирования, проектирования микроэлектронных схем и телекоммуникационных систем. Для описания поведения систем реального времени модель конечного автомата может быть расширена добавлением в неё часов - параметра непрерывного времени, моделируемого вещественной переменной. В автоматах реального времени для входных и выходных сигналов указывается время их поступления и выдачи, а переходы автомата снабжены описанием задержек, связанных с ожиданием входных сигналов и формированием выходных сигналов. Так же, как и для классических автоматов дискретного времени, задача минимизации конечных автоматов реального времени возникает во многих приложениях этой модели вычислений. Для классической модели автоматов реального времени эта задача уже подробно рассмотрена. В нашей работе мы предлагаем более сложную модель: в ней порядок следования выходных сигналов определяется не только порядком поступления входных сигналов, но также и задержкой, связанной с их обработкой. В этой модели при выполнении одной и той же последовательности переходов выходные сигналы могут выдаваться в разном порядке в зависимости от времени поступления входных сигналов. В новой модели автоматов реального времени решению задачи минимизации должно предшествовать изучение вопроса строгой детерминированности - однозначности поведения автомата на одних и тех же последовательностях переходов. В представленной статье приведены и обоснованы необходимые и достаточные условия строгой детерминированности автоматов реального времени, а также исследованы вопросы, связанные с решением задачи минимизации этой разновидности автоматов.