Последовательные реагирующие системы - это формальные модели программ, которые взаимодействуют с окружающей средой, получая входные данные и производя соответствующие выходы. Такие формальные модели широко используются в программной инженерии, компьютерной лингвистике, телекоммуникациях и т. д. В реальной жизни поведение реагирующей системы зависит не только от потока входных данных, но также от времени поступления входных данных и задержек, которые возникают при генерации ответов. Чтобы зафиксировать эти аспекты, в качестве формальной модели последовательной реактивной системы в реальном времени используется временный конечный автомат (TFSM). Однако в большинстве известных предыдущих работ эта модель рассматривалась в упрощенной семантике: отклики в потоке на выходе машины, независимо от их временных меток, следуют в том же порядке, в котором соответствующие входные данные доставляются в машину. Это упрощение облегчает анализ модели, но упускает из виду многие важные аспекты вычислений в реальном времени. В этой статье мы изучаем более строгую семантику TFSM и показываем, как ее представить с помощью систем помеченных переходов. Это открывает возможность применения традиционных формальных методов для проверки более тонких свойств реагирующего поведения в реальном времени, которые ранее игнорировались.