Автомат с синхронизацией по времени

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

Временные автоматы могут использоваться для моделирования и анализа временного поведения компьютерных систем, например систем или сетей реального времени. Методы проверки свойств безопасности и живучести были разработаны и интенсивно изучаются в течение последних 20 лет.

Было показано, что проблема достижимости состояний для временных автоматов разрешима ^[1], что делает этот подкласс гибридных автоматов интересным. Расширения были тщательно изучены, в том числе секундомеры, задачи в реальном времени, функции затрат и игры с таймером. Существует множество инструментов для ввода и анализа временных автоматов и расширений, включая средства проверки моделей UPPAAL , Kronos и анализатор планируемости TIMES. Эти инструменты становятся все более зрелыми, но все еще остаются инструментами академических исследований.

Пример [ править ]

Прежде чем формально определить, что такое синхронизированный автомат, приведем несколько примеров.

Рассмотрит язык из приуроченных-слов над одноместный алфавитом , например , что существует в течение первой единицы времени, и меньше , чем один раз блок между двумя последовательными . Автомат с синхронизацией, распознающий этот язык, изображенный рядом, использует одни часы , которые никогда не должны равняться единице. Эти часы отсчитывают время с начала прогона, если не было сгенерировано, или с момента последнего срабатывания в противном случае. Это означает, что каждый раз, когда выдается an , эти часы сбрасываются на ноль.${\displaystyle {\mathcal {L}}}$ ${\displaystyle w}$${\displaystyle \{a\}}$${\displaystyle a}$${\displaystyle a}$ ${\displaystyle x}$${\displaystyle a}$${\displaystyle a}$${\displaystyle a}$

Синхронизированный автомат, принимающий язык a *, такой, что буква излучается в каждом открытом интервале длины один.

Рассмотрим язык из приуроченных-слов над двоичным алфавитом , так что каждый сопровождается в следующем единицу времени. Автомат с синхронизацией, распознающий этот язык, изображенный рядом, вспоминает, существовал ли а, за которым не следовала а, или нет. Если это не так, он принимает запуск, в противном случае он отклоняет его. Кроме того, когда есть такой , у него есть часы, которые вспоминают время, прошедшее с тех пор, как был выпущен первый такой . В этом случае не может быть выдано a, если часы, по крайней мере, равны единице, и, таким образом, запуск завершается ошибкой.${\displaystyle {\mathcal {L}}}$ ${\displaystyle w}$${\displaystyle \{a,b\}}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle x}$${\displaystyle a}$${\displaystyle b}$

Синхронизированный автомат, принимающий синхронизированные слова, в которых за каждым появлением следуют менее одной единицы времени после появления .${\displaystyle \{a,b\}}$${\displaystyle a}$${\displaystyle b}$

Формальное определение [ править ]

Автомат с синхронизацией [ править ]

Формально синхронизированный автомат - это кортеж , состоящий из следующих компонентов:${\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle }$

• ${\displaystyle \Sigma }$конечное множество называется алфавитом или действия из .${\displaystyle {\mathcal {A}}}$
• ${\displaystyle L}$- конечное множество . Элементы называются местоположениями или состояниями .${\displaystyle L}$${\displaystyle {\mathcal {A}}}$
• ${\displaystyle L_{0}\subseteq L}$ - это набор начальных местоположений.
• ${\displaystyle C}$конечное множество называют часы из .${\displaystyle {\mathcal {A}}}$
• ${\displaystyle F\subseteq L}$ - это набор принимающих местоположений.
• ${\displaystyle E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\times {\mathcal {P}}(C)\times L}$представляет собой набор ребер, называется переходы из , где${\displaystyle {\mathcal {A}}}$
  • ${\displaystyle {\mathcal {B}}(C)}$- набор ограничений часов, включающих часы из , и${\displaystyle C}$
  • ${\displaystyle {\mathcal {P}}(C)}$является Powerset из .${\displaystyle C}$

Края от происходит переход от местоположений , чтобы с действием , охраны и часы сброса .${\displaystyle (\ell ,\sigma ,g,r,\ell ')}$${\displaystyle E}$${\displaystyle \ell }$${\displaystyle \ell '}$${\displaystyle \sigma }$${\displaystyle g}$${\displaystyle r}$

Расширенное состояние [ править ]

Пара с местоположением и оценкой часов называется расширенным состоянием или состоянием .${\displaystyle \ell }$ ${\displaystyle \nu }$

Обратите внимание, что слово состояние, таким образом, неоднозначно, поскольку, в зависимости от автора, оно может означать либо пару, либо элемент . Для ясности в этой статье мы будем использовать термин местоположение для элемента и термин расширенное местоположение для пар.${\displaystyle L}$${\displaystyle L}$

В этом заключается одно из самых больших различий между временными автоматами и конечными автоматами . В конечном автомате в какой-то момент выполнения состояние полностью описывается числом прочитанных букв и конечным числом возможных значений, которые на самом деле называются «состояниями». Это означает, что с учетом состояния и суффикса читаемого слова оставшаяся часть выполнения полностью определяется. Таким образом, слово «конечный» в названии «конечный автомат». Однако, как объясняется в разделе «Выполнение» ниже, для возобновления работы тактовой частоты используются часы для определения того, какие переходы могут быть выполнены. Таким образом, чтобы узнать состояние автомата, вы должны знать, в каком месте вы находитесь, и оценку часов.

Выполнить [ редактировать ]

Учитывая синхронизированное слово с , возрастающую последовательность неотрицательных чисел и синхронизированный автомат, как указано выше, запуск представляет собой последовательность формы, удовлетворяющую следующему ограничению:${\displaystyle w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots ,}$${\displaystyle \sigma _{i}\in \Sigma }$${\displaystyle (t_{i})_{i}}$${\displaystyle {\mathcal {A}}}$${\displaystyle (\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots }$

• (инициализация) ${\displaystyle \ell _{0}\in L_{0}}$
• (последовательность) для всех существует такое ребро формы , что:${\displaystyle i\geq 1}$${\displaystyle E}$${\displaystyle \langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle }$
  • мы предполагаем, что единицы времени прошли, и в это время охранник доволен. Т.е. удовлетворяет ,${\displaystyle t_{i}-t_{i-1}}$${\displaystyle \nu _{i-1}+t_{i}-t_{i-1}}$${\displaystyle g_{i}}$
  • новая оценка часов соответствует тому , в какие единицы времени прошли и в какие часы сбрасываются. Формально .${\displaystyle \nu _{i}}$${\displaystyle \nu _{i-1}}$${\displaystyle t_{i}-t_{i-1}}$${\displaystyle r_{i}}$${\displaystyle \nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]}$

Понятие принимающего пробега определяется как в конечных автоматах для конечных слов и как в автоматах Бюхи для бесконечных слов. То есть, если длина конечна , то пробег считается допустимым, если . Если слово бесконечно, то пробег принимается тогда и только тогда, когда существует бесконечное количество позиций, таких что .${\displaystyle w}$${\displaystyle n}$${\displaystyle \ell _{n}\in F}$${\displaystyle i}$${\displaystyle \ell _{i}\in F}$

Детерминированный синхронизированный автомат [ править ]

Как и в случае конечного автомата и автомата Бюхи, синхронизированный автомат может быть детерминированным или недетерминированным. Интуитивно детерминированность имеет одно и то же значение в каждом из этих случаев. Это означает, что набор начальных местоположений является одноэлементным, и что, учитывая состояние и букву , существует только одно возможное состояние, из которого можно достичь путем чтения . Однако в случае с автоматом по времени формальное определение немного сложнее. Формально таймер детерминирован, если:${\displaystyle s}$${\displaystyle a}$${\displaystyle s}$${\displaystyle a}$

• ${\displaystyle L_{0}}$ это синглтон
• для каждой пары переходов и множество оценок часов, которым удовлетворяют, не пересекаются с множеством оценок часов, которым удовлетворяют .${\displaystyle (\ell ,\sigma ,g,r,\ell ')}$${\displaystyle (\ell ,\sigma ,g',r',\ell '')}$${\displaystyle g}$${\displaystyle g'}$

Свойство закрытия [ править ]

Класс языков, распознаваемых недетерминированными временными автоматами:

• замкнутое относительно объединения, действительно, несвязное объединение двух временных автоматов распознает объединение языка, распознаваемого этими автоматами.
• закрыто под перекрестком. ^[2]
• не закрывается при дополнении. ^[3]

Проблемы и их сложность [ править ]

Приведена вычислительная сложность некоторых задач, связанных с временными автоматами.

Проблему пустоты для синхронизированного автомата можно решить, построив региональный автомат и проверив, принимает ли он пустой язык. Эта проблема решена для PSPACE . ^{[1] : 207}

The universality problem of non-deterministic timed automaton is undecidable, and more precisely Π11. However, when the automaton contains a single clock, the property is decidable, however it is not primitive recursive.^[3] This problem consists in deciding whether every words are accepted by a timed-automaton.

See also[edit]

• Alternating timed automaton: an extension of timed automaton with universal transitions.

Notes[edit]