Темпоральний автомат

Темпоральний автомат^{[усталений термін?]} в теорії автоматів — скінченний автомат, розширений скінченною множиною годинникових змінних. Годинникові змінні приймають дійсні значення та призначені для виміру часових характеристик.

Темпоральні автомати використовуються для моделювання скінченних систем реального часу.

Формальне визначення

Темпоральний автомат може бути визначений як кортеж, що складається з 8 елементів( L, L₀, E, A, C, T, G, I )^{[джерело?]}:

непуста скінчена множина позицій L;
початкова позиція L₀, що є елементом множини L;
множина ребер Е, кожне з яких має помітки, що вказують, з якої позиції виходить дане ребро і в яке входить;
функція A, яка відображає позицію у множину атомарних речень;
скінчена множина годинників C;
функція T, яка відображає ребро у множину годинників;
функція G, яка відображає ребро у часове обмеження;
функція I, яка відображає позицію в інваріант.

Обчислення автомата

Крок обчислення темпорального автомату складається з просування часу, виконання переходу та перевірки інваріантів^{[джерело?]}.

Просування часу: Значення всіх годинників збільшуються на деяку однакову константу, а поточна позиція автомату не змінюється.

Виконання переходу: Обирається активний перехід із L_s в L_d . Умовою активності переходу є виконання відповідних часових обмежень. Поточною позицією автомату стає L_d. Годинникові змінні, які відповідають обраному переходу, ініціалізуються.

Перевірка інваріантів: Інваріанти, які відповідають усім позиціям автомату, повинні бути виконані.

Приклад

Приклад темпорального автомату для пристрою перемикання наведено на рисунку.

Приклад темпорального автомату

Позиція S0 відповідає вимкненому стану пристрою, а S1 – увімкненому. Пристрій вимикається через 13 часових одиниць після перемикання із вимкненого стану перемикача в увімкнений стан. Це вимикання контролюється годинником y. Годинник x використано для моделювання того, що прилад може бути увімкнений як мінімум через 3 часових одиниць після перемикання.

Література

Hopcroft, John E.; Motwani, Rajeev; Ullman, Jeffrey D. (2001). Вступ до теорії автоматів, мов і обчислень (вид. 2nd). Addison–Wesley. с. 521.(англ.)
Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. - СПб : Наука, 2011.- 244 с. - ISBN 978-5-02-038160-5. (рос.)
Alur, R. and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183-235. (англ.)