Автомат с таймером

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

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

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

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

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

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

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

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

Автомат с таймером [ править ]

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

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

Край $(\ell ,\sigma ,g,r,\ell ')$ от $E$ это переход из локаций $\ell$ к $\ell '$ с действием $\sigma$ , сторожить $g$ и часы сбрасываются $r$ .

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

Пара с локацией $\ell$ и оценка часов $\nu$ называется либо расширенным состоянием , либо состоянием .

Заметим, что слово состояние при этом неоднозначно, поскольку, в зависимости от автора, оно может обозначать либо пару, либо элемент $L$ . Для ясности в этой статье будет использоваться термин «расположение ». для обозначения элемента $L$ и термин «расширенное местоположение» для пар.

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

Беги [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также [ править ]

Попеременный автомат с таймером : расширение таймера с универсальными переходами.

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

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

[AlurDill-1] Jump up to: Перейти обратно: ^а ^б Раджив Алур, Дэвид Л. Дилл. 1994 Теория временных автоматов . В «Теоретической информатике» , вып. 126, 183–235, стр. 194–1955.

[2] Современные применения автоматов, стр. 118.

[Alternating_timed_automata-3] Jump up to: Перейти обратно: ^а ^б Ласота, Савомир; Валукевич, Игорь (2008). «Попеременные временные автоматы». Транзакции ACM в вычислительной логике . 9 (2): 1–26. arXiv : cs/0512031 . дои : 10.1145/1342991.1342994 . S2CID 12319 .

[1]

[2]

[3]