Темпоральний автомат в теорії автоматів — скінченний автомат, розширений скінченною множиною годинникових змінних. Годинникові змінні приймають дійсні значення та призначені для виміру часових характеристик.
Темпоральні автомати використовуються для моделювання скінченних систем реального часу.
Формальне визначення Темпоральний автомат може бути визначений як кортеж, що складається з 8 елементів( L, L0, E, A, C, T, G, I ): непуста скінчена множина позицій L; початкова позиція L0, що є елементом множини L; множина ребер Е, кожне з яких має помітки, що вказують, з якої позиції виходить дане ребро і в яке входить; функція A, яка відображає позицію у множину атомарних речень; скінчена множина годинників C; функція T, яка відображає ребро у множину годинників; функція G, яка відображає ребро у часове обмеження; функція I, яка відображає позицію в інваріант.
Обчислення автомата Крок обчислення темпорального автомата складається з просування часу, виконання переходу та перевірки інваріантів.
Просування часу: Значення всіх годинників збільшуються на деяку однакову константу, а поточна позиція автомата не змінюється.
Виконання переходу: Обирається активний перехід із Ls в Ld . Умовою активності переходу є виконання відповідних часових обмежень. Поточною позицією автомата стає Ld. Годинникові змінні, які відповідають обраному переходу, ініціалізуються.
Перевірка інваріантів: Інваріанти, які відповідають усім позиціям автомата, повинні бути виконані.
Приклад Приклад темпорального автомата для пристрою перемикання наведено на рисунку.
Позиція S0 відповідає вимкненому стану пристрою, а S1 – увімкненому. Пристрій вимикається через 13 часових одиниць після перемикання із вимкненого стану перемикача в увімкнений стан. Це вимикання контролюється годинником y. Годинник x використано для моделювання того, що прилад може бути увімкнений як мінімум через 3 часових одиниць після перемикання.
Література
Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. - СПб : Наука, 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.