Remark: We consider only the next-free fragment of LTL.

CTL formula:

CtlFormula:	AtomicProposition
	| UnOp CtlFormula
	| CtlFormula BinOp CtlFormula
	| PathQuantifier TempOp CtlFormula (not for U)
	| PathQuantifier [ CtlFormula U CtlFormula ]
	| ( CtlFormula )

LTL formula:

LtlFormula:	AtomicProposition
	| UnOp LtlFormula
	| LtlFormula BinOp LtlFormula
	| TempOp LtlFormula (not for U)
	| LtlFormula U LtlFormula
	| ( LtlFormula )

Logical operators:

UnOp:	!                      (negation)
	| -                    (negation)
BinOp:	&                  (conjunction)
	| *                    (conjunction)
	| |                   (disjunction)
	| +                   (disjunction)
	| =>                (implication)

Temporal operators:

TempOp:	G                      (globally)
	| F                      (eventually)
	| U                     (until)
	| X                     (next)

Path quantifiers (only CTL):

PathQuantifier:	A                      (On all paths ...)
	| E                      (There exists a path ...)

Atomic propositions:

The atomic propositions are different for each input language.
See APNN, B(PN)^2, CFA, IF, PEP, SENIL.