| progr. | in the definition of timed automaton, we allowed the clock constraints that serve as the invariants of locations and the guards of transitions to contain arbitrary rational constants | в определении временного автомата мы допускали использование временных ограничений в качестве инвариантов позиций и предохранителей переходов, содержащих произвольные рациональные константы (см. Model Checking / Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled 1999) |