| Russian | English |
| в определении временного автомата мы допускали использование временных ограничений в качестве инвариантов позиций и предохранителей переходов, содержащих произвольные рациональные константы | 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) |
| временное ограничение инварианта позиции или предохранителя перехода | clock constraint in the invariant of a location or in the guard of a transition (ssn) |
| если действием некоторого перехода будет действие только одного из двух процессов, то для каждой позиции второго временного автомата в параллельной композиции будет совместный переход | if the action of a transition is only an action of one of the two processes, then there will be a transition in the parallel composition for each location of the other timed automaton (см. Model Checking / Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled 1999 ssn) |
| одна и та же позиция временного автомата | same location of the timed automaton (ssn) |
| отображение позиций во временные ограничения | mapping from locations to clock constraints (ssn) |
| отображение позиций во временные ограничения, называемое инвариантом позиций | mapping from locations to clock constraints, called the location invariant (ssn) |
