Computation tree logic
= Computation tree logic
{wiki}
= CTL
{c}
{synonym}
A branching <temporal logic> whose operators quantify over <paths in a transition system> from a <state>. In particular, $AG\Phi$, also written $\forall\square\Phi$, holds at $s$ when every infinite <path in a transition system> from $s$ satisfies $\Phi$ at every position, including its initial position.