Синтез установочных последовательностей для автоматов с временными ограничениями

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