The form of supported CTL formulas is presented below in EBNF.
<CTL> ::= <P>
<P> ::= <T> | <P>' AND '<P> | <P>' OR '<P> | '('<P>')'
| 'NOT ('<P>')' | <A>
<T> ::= 'EX('<P>')' | 'EF('<P>')' | 'EG('<P>')' | 'E[('<P>') U ('<P>')]'
| 'E[('<P>') R ('<P>')]' | 'AX('<P>')' | 'AF('<P>')' | 'AG('<P>')'
| 'A[('<P>') U ('<P>')]' | 'A[('<P>') R ('<P>')]'
<A> ::= 'm(p'<N>')='<M> | 'true' | 'false'
<N> ::= positive integer representing place number
<M> ::= nonnegative integer representing token number