Lineárna temporálna logika

• casová os:

  • dvojica (S, ?), kde ? je úplné usporiadanie
  • izomorfná s (?, <)

• cas:

  • diskrétny
  • pociatocný okamih
  • nekonecný

• AP: atomické propozície (ozn. P, Q, …)

• štruktúra lineárneho casu: trojica M = (S, x, L), kde

S ? mnozina stavov

x: ? ? S ? postupnost stavov

L: S ? ?(AP) ? urcuje pre daný stav, ktoré atomické propozície v tomto stave platia (teda ktoré AP sú true)

• oznacenie:

  • postupnost stavov x = s0, s1, s2, s3, …
  • definujeme xi = si, si+1, si+2, si+3, … (teda x = x0)

• základné temporálne operátory:

?p ? eventually p (raz urcite p) (textovo Fp)

?p ? vzdy p (textovo Gp)

?p ? nasledujúci krát p (textovo Xp)

p ? q ? p until q (q zacne platit, ked p prestane)

Previous slide

Next slide

Back to first slide

View graphic version