Система преобразования автоматной модели в модель Крипке и верификация CTL-свойств на ней