Model Checking для CTL AXϕ выполняется в состоянии s , если формула ϕ выполняется во всех состояниях, непосредственно следующих за s ;
EXϕ выполняется в состоянии s , если формула ϕ выполняется хотя бы в одном состоянии, непосредственно следующем за s ;
AFϕ (неизбежно ϕ ) выполняется в состоянии s , если на всех путях, начинающихся из состояния s , формула ϕ когда-нибудь выполнится;
EFϕ (возможно ϕ ) выполняется в состоянии s , если из этого состояния существует путь, на котором формула ϕ когда-нибудь выполнится;
AGϕ (глобально ϕ ) выполняется в состоянии s , если на всех путях, начинающихся из состояния s , во всех состояниях этих путей формула ϕ выполняется;
EGϕ выполняется в состоянии s , если существует путь из s , во всех состояниях которого формула ϕ выполняется;
A(ϕ1Uϕ2 ) выполняется в состоянии s , если на всех путях, начинающихся в s , когда-нибудь в будущем выполнится формула ϕ2 , а до этого во всех состояниях этих путей выполняется формула ϕ1 ;
E (ϕ1Uϕ2) выполняется в состоянии s , если из s существует путь, на котором когда-нибудь в будущем выполнится ϕ2 , а до этого во всех состояниях этого пути выполняется ϕ1 .