В проверке моделей , подполе информатики , синхронизированное слово является расширением понятия слов на формальном языке , в котором каждая буква связана с положительной меткой времени. Последовательность меток времени должна быть неубывающей , что интуитивно означает, что буквы принимаются. Например, система, принимающая слово по сети, может связывать с каждой буквой время, в которое письмо было получено. Условие неубывания здесь означает, что письма получены в правильном порядке.
Приуроченный язык представляет собой набор синхронизированных слов.
Пример
Рассмотрим лифт. То, что формально называется письмом, на самом деле может быть такой информацией, как «кто-то нажимает кнопку на 2-м этаже» или «двери открываются на третьем этаже». В этом случае синхронизированное слово - это последовательность действий, предпринятых лифтом и его пользователями, с отметками времени, чтобы вспомнить эти действия. Затем синхронизированное слово может быть проанализировано формальным методом, чтобы проверить, выполняется ли свойство, такое, что «каждый раз, когда лифт вызывается, он прибывает менее чем за три минуты при условии, что никто не удерживал дверь более пятнадцати секунд». Утверждение, подобное этому, обычно выражается в метрической временной логике , расширении линейной временной логики, которая позволяет выражать временные ограничения.
Синхронизированное слово может быть передано модели, такой как синхронизированный автомат , который решит, учитывая буквы или действия, которые уже произошли, какое действие должно быть выполнено следующим образом. В нашем примере, на какой этаж должен идти лифт. Затем программа может протестировать этот синхронизированный автомат и проверить вышеупомянутое свойство. То есть он попытается сгенерировать синхронизированное слово, в котором дверь никогда не остается открытой более пятнадцати секунд, и в котором пользователь должен ждать более трех минут после вызова лифта.
Определение
Для данного алфавита A синхронизированное слово представляет собой последовательность, конечную или бесконечную с участием , с участием для каждого целого числа .
Если последовательность бесконечна, но последовательность ограничено, то это слово называется синхронизированным словом Зенона., [1] в отношении парадоксов Зенона, где бесконечное количество действий происходит за конечное время.
Не вовремя это слово без отметок времени, т.е. . Учитывая синхронизированный язык, Без сроков тогда набор безвременных для .
Рекомендации
- ^ Estévenart, Morgane (сентябрь 2015). «2». Проверка и синтез MITL через чередующиеся временные автоматы (PhD). п. 56.
- Алур, Раджив; Укроп, Дэвид (1994). «Теория автоматизированных автоматов». Теоретическая информатика . 126 : 190.