# What's the definition of ACTL?

I have been looking for the definition of ACTL, but Google has given me very little to go with.

So far, I know ACTL is another form of CTL model checking, and CTL includes the following operators:

• Always
• Exist
• Global
• Finally
• Next
• AND / OR
• NOT

So what does ACTL include and how is it different from CTL?

Many thanks

ACTL is the universal fragment of CTL. Thus, existential path quantification is not allowed. So a path formula is of the form $AF\psi$, $AG\psi$, or $AX\psi$ (or a conjunction or disjunction of path formulas).
• You can't write $\neg AGp$, since it's equivalent to $EF\neg p$, so you get an $E$ operator. Negations are only allowed on the inner proposition, e.g. $AG\neg p$. May 21, 2016 at 7:28
• @N.S. ACTL is weaker than LTL: an LTL formula can say something like FGp (or, with the explicit quantifier: AFGp), which means "all paths must have finitely many $\neg p$". This cannot be captured in CTL (requires proof), because intuitively you can only say something like AFAGp, meaning that in all paths you eventually reach a state from which all paths always labelled p. But this is a stronger requirement, as it implies a "uniform" bound on the eventuality. Jun 17, 2022 at 18:29