3
$\begingroup$

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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\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, 2016 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, 2016 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, 2016 at 8:59
  • $\begingroup$ So how does ACTL differ from LTL, given that LTL formulas can be thought of as having an implicit A in front of them? $\endgroup$
    – Motorhead
    Jun 17, 2022 at 17:28
  • $\begingroup$ @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. $\endgroup$
    – Shaull
    Jun 17, 2022 at 18:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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