# 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$. – Shaull May 21 '16 at 7:28