Автомат с синхронизацией - Timed automaton

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

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

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

Пример

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

Рассмотрим язык ${\displaystyle {\mathcal {L}}}$ из своевременные слова ${\displaystyle w}$ над унарным алфавитом ${\displaystyle \{a\}}$ так что есть ${\displaystyle a}$ в течение первой единицы времени, а между двумя последовательными ${\displaystyle a}$. Автомат с синхронизацией по времени, распознающий этот язык, изображенный рядом, использует один Часы ${\displaystyle x}$, который никогда не должен быть равен единице. Эти часы отсчитывают время с начала пробега, если нет ${\displaystyle a}$ были выпущены, или с последнего ${\displaystyle a}$ испускается иначе. Это означает, что каждый раз ${\displaystyle 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 C}$ конечное множество, называемое часы из ${\displaystyle {\mathcal {A}}}$.
• ${\displaystyle L_{0}\subseteq L}$ - это набор начальных местоположений.
• ${\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]}$.

Понятие принятия пробега определяется как в конечные автоматы для конечных слов и как в Büchi автоматы для бесконечных слов. То есть, если ${\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

Проблема универсальности недетерминированного временного автомата неразрешима, а точнее Π¹
₁. Однако, если автомат содержит одни часы, свойство разрешимо, но не примитивно рекурсивный.^[3] Эта проблема состоит в том, чтобы решить, принимаются ли все слова автоматом по времени.

Смотрите также

• Автомат с переменным временем: расширение синхронизированного автомата с универсальными переходами.

Примечания

1. Раджив Алур, Дэвид Л. Дилл. 1994 г. Теория временных автоматов. В теоретической информатике, т. 126, 183–235, стр. 194–1955.
2. Современные приложения автоматов, страница 118
3. Ласота, Славомир; Валукевич, Игорь (2008). «Чередующиеся временные автоматы». Транзакции ACM по вычислительной логике. 9 (2): 1–26. arXiv:cs / 0512031. Дои:10.1145/1342991.1342994.