Синхронизированное слово - Timed word

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

А синхронизированный язык представляет собой набор синхронизированных слов.

Пример

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

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

Определение

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

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

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

Рекомендации

1. Эстевенар, Морган (сентябрь 2015 г.). «2». Проверка и синтез MITL через чередующиеся временные автоматы (Кандидат наук). п. 56.

• Алур, Раджив; Укроп, Дэвид (1994). «Теория автоматизированных автоматов». Теоретическая информатика. 126: 190.