Propozicná lineárna temporálna logika

• Syntax: mnozina PLTL formúl je definovaná ako najmenšia mnozina generovaná nasledujúcimi pravidlami:

  • kazdá AP (atomická propozícia) P je formula
  • ak p, q sú formuly, tak p ? q, ?p sú formuly
  • ak p, q sú formuly, tak p ? q, ?p (Xp) sú formuly

potom mozno zaviest oznacenia

Fp = true ? p ?p

Gp = ?F?p ?p

F?p = GFp (nekonecne vela krát)

G?p = FGp (skoro všade)

• Sémantika:

x ? P iff P ? L(s0) pre atomickú propozíciu P

x ? p ? q iff platí x ? p and x ? q

x ? ?p iff neplatí x ? p

x ? (p ? q) iff ?j (xj ? q and ?k < j: xk ? p)

x ? Xp iff x1 ? p

x ? Fp iff ?j (xj ? p)

x ? Gp iff ?j (xj ? p)

x ? F?p iff ?k ?j ? k (xj ? p)

x ? G?p iff ?k ?j > k (xj ? p)

• Príklady:

  G(p ? Fq): vzdy ked platí p, tak raz zacne platit aj q
  
  p ? G(p ? Xq) ? Gp: temporálna formulácia indukcie
  p ? Fq: ak p platí teraz, tak raz bude platit q

Previous slide

Next slide

Back to first slide

View graphic version