Приведен обзор логики CTL и ее применения для формальной верификации. Предложена логика Х-CTL, позволяющая осуществлять формальную верификацию Х-машин. Приведен пример модели-счетчика.