Бұл жүйе үшін барлық мүмкін болатын өткелдер өткелдің төрт жағдайымен анықталады

2. тек қасқыр;

немесе

3. тек ешкі;

немесе

4. тек қырыққабат.

CTL үшін Model Checking символдық алгоритмы

CTL үшін model checking әдісімен верификациялау міндеті келесіден тұрады: Крипке М құрылымы және тармақталған уақыт логикасының (CTL) темпоралдық формуласы берілген. Ф орындалатын Крипке М құрылымының көптеген жағдайларын табу . Егер бастапқы жағдай S0 болса , онда Ф М үшін орындалады .