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).

Moreover, you are not allowed a general NOT operator, but rather negations have to be on the atomic propositions (otherwise this fragment would be equal to CTL).