Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Model-Checking Kit: Syntax of CTL and LTL

 

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.