patternMinor
What's the definition of ACTL?
Viewed 0 times
definitiontheactlwhat
Problem
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:
So what does ACTL include and how is it different from CTL?
Many thanks
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
Solution
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).
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).
Context
StackExchange Computer Science Q#57695, answer score: 4
Revisions (0)
No revisions yet.