| English | Russian |
| A simple and effective way to allow the verification of time bounded properties is to introduce bounds in the CTL temporal operators | Простой и эффективный способ, позволяющий верифицировать свойства с ограничениями по времени, состоит в том, чтобы внести эти ограничения в темпоральные операторы CTL (см. Model Checking / Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled 1999 ssn) |
| algorithms for CTL model checking | алгоритмы верификации моделей для формул CTL (ssn) |
| algorithms for CTL model checking, LTL model checking | алгоритмы верификации моделей для формул CTL и для формул LTL (ssn) |
| algorithms for CTL model checking, LTL model checking, and testing inclusion between timed omega automata | алгоритмы верификации моделей для формул CTL и для формул LTL, а также проверки включения временных омега-автоматов (ssn) |
| CTL model checking algorithm | алгоритм верификации моделей для CTL (ssn) |
| CTL symbolic model checking | символьная верификация моделей для CTL (Computation Tree Logic ssn) |
| CTL symbolic model checking algorithm | алгоритм символьной верификации моделей для CTL (Computation Tree Logic ssn) |
