Приуроченное слово

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

Синхронный язык – это набор синхронизированных слов.

Пример

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

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

Определение

Учитывая алфавит A , синхронизированное слово представляет собой последовательность, конечную или бесконечную. $w=(a_{0},t_{0})(a_{1},t_{1})\dots$ с $a_{i}\in A$, $t_{i}\in \mathbb {R} _{+}$ с $t_{i}\leq t_{i+1}$ для каждого целого числа $i$.

Если последовательность бесконечна, но последовательность $(t_{0})(t_{1})\dots$ ограничено, то это слово называется словом Зенона , в отношении парадоксов Зенона , где бесконечное количество действий происходит за конечное время.

Слово $\operatorname {untimed} (w)$ это слово $w$ без отметок времени, т.е. это $a_{0}a_{1}\dots$. Учитывая временной язык $L$, $\operatorname {untimed} (L)$ тогда это набор $\operatorname {untimed} (w)$ для $w\in L$.

Ссылки

• Алур, Раджив ; Дилл, Дэвид (1994). «Теория синхронизированных автоматов» . Теоретическая информатика . 126 (2): 190. дои : 10.1016/0304-3975(94)90010-8 .