Logika LTL

Logika LTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.

PLTL

Jest to odmiana logiki LTL oparta na rachunku zdań (bazująca wyłącznie na zmiennych zdaniowych).

Struktura czasu

Strukturą czasu w PLTL jest struktura M=(S,X,L), gdzie:

  • S – zbiór stanów: S={s0,s1,s2,...},
  • X – nieskończona ścieżka stanów: X=(s0,s1,s2,...),
  • L – wartościowanie (przypisanie każdemu ze stanów wyrażeń, które są prawdziwe w tym stanie) L:S×WA→{0,1}, WA – zbiór wyrażeń atomowych

Język

  • zmienne zdaniowe p,q,r,…
  • spójniki zdaniowe rachunku zdań:
    • koniunkcja (∧),
    • alternatywa (∨),
    • implikacja (⇒),
    • równoważność (⇔),
    • negacja (¬)
  • operatory temporalne:
    • U – αUβ oznacza, że w pewnym momencie w przyszłości będzie prawdziwe β, a do tego momentu będzie prawdziwe α
    • R – αRβ oznacza, że β będzie prawdziwe dopóki nie zacznie być prawdziwe α (αRβ≡¬(¬αU¬β))
    • X – Xα oznacza, że α będzie prawdziwe w następnym momencie (oznaczany też jako ∘)
    • G – Gα oznacza, że α jest prawdziwe w każdym momencie (Gα≡αU⊥)
    • F – Fα oznacza, że α będzie prawdziwe w pewnym momencie w przyszłości (Fα≡⊤Uα)
    • F∞ – F∞α oznacza, że α będzie prawdziwe w przyszłości w nieskończenie wielu momentach (zawsze z wyjątkiem pewnej skończonej liczby momentów) (F∞α≡GFα)
    • G∞ – G∞α oznacza, że α będzie prawdziwe od pewnego momentu w przyszłości (G∞α≡FGα)
  • nawiasy

Formuły

Niech WA będzie zbiorem wyrażeń atomowych.

  • każde wyrażenie α∈WA jest formułą
  • jeśli α i β są formułami, to α∧β i ¬α też są formułami
  • jeśli α i β są formułami, to αUβ i Xα też są formułami

Prawdziwość formuł

  • Oznaczenia:

(M,x)⊨α – formuła α jest prawdziwa w strukturze M na ścieżce x
(M,si)⊨α – formuła α jest prawdziwa w strukturze M w stanie si

  • warunki prawdziwości podstawowych formuł:

(M,si)⊨p⇔p∈L(si)
(M,si)⊨(α∧β)⇔((M,si)⊨α)∧((M,si)⊨β)
(M,si)⊨¬α⇔¬(M,si)⊨α
(M,si)⊨αUβ⇔∃k>i(M,sk)⊨β∧(∀j:(i⩽j<k)(M,sj)⊨α))
(M,si)⊨Xα⇔(M,si+1)⊨α

PLTLFO

Odmiana logiki LTL oparta na rachunku predykatów pierwszego rzędu.

Język

  • wszystkie elementy PLTL
  • kwantyfikatory – ∀,∃
  • znak równości =
  • symbole predykatywne P,Q,R,…
  • symbole funkcyjne f,g,h,…
  • symbole stałe c1,c2,…
  • zmienne x1,x2,…

Formuły

  • termy:
    • zmienne,
    • stałe,
    • wyrażenia postaci: f(t1,t2,…,tn), gdzie ti są stałymi bądź zmiennymi
  • predykaty:
    • wyrażenia postaci: P(t1,t2,…,tn), gdzie ti są stałymi bądź zmiennymi
  • atomy:
    • stałe,
    • predykaty,
    • wyrażenia postaci: t1=t2, gdzie t1 i t2 są stałymi bądź zmiennymi
  • formuły:
    • takie, jak w PLTL,
    • atomy,
    • wyrażenia postaci: ∀x α oraz ∃x α, gdzie α jest formułą, a x jest zmienną.

Linki zewnętrzne