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

| cite | improve this answer | |
  • $\begingroup$ so E operator is not allowed, but can you give an example for the second part with NOT operator? $\endgroup$ – Thang Do May 21 '16 at 7:11
  • 1
    $\begingroup$ 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$. $\endgroup$ – Shaull May 21 '16 at 7:28
  • $\begingroup$ that was so much easier to understand than reading through article on Google. Thank heaps, Shaull $\endgroup$ – Thang Do May 21 '16 at 8:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.