Logika LTL

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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


PLTL[edytuj | edytuj kod]

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

Struktura czasu[edytuj | edytuj kod]

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

  •  S - zbiór stanów:  S=\{s_{0}, s_{1}, s_{2},...\},
  •  X - nieskończona ścieżka stanów:  X=(s_{0}, s_{1}, s_{2},...),
  •  L - wartościowanie (przypisanie każdemu ze stanów wyrażeń, które są prawdziwe w tym stanie)  L:S \times WA \rightarrow \{0,1\} ,  WA - zbiór wyrażeń atomowych)


Język[edytuj | edytuj kod]

  • zmienne zdaniowe  p, q, r, \ldots
  • spójniki zdaniowe rachunku zdań:
    • koniukcja (  \wedge ) ,
    • alternatywa (    \vee  ) ,
    • implikacja (   \Rightarrow ) ,
    • równoważność(   \Leftrightarrow  ) ,
    • negacja (  \neg )
  • operatory temporalne:
    •  U -  \alpha U \beta  oznacza, że w pewnym momencie w przyszłości będzie prawdziwe \beta, a do tego momentu będzie prawdziwe  \alpha
    •  R -  \alpha R \beta  oznacza, że w pewnym momencie w przyszłości będzie prawdziwe \beta, a do tego momentu będzie prawdziwe \alpha
      (  \alpha R \beta   \equiv \neg (\neg \alpha U \neg \beta)  )
    •  X -  X \alpha oznacza, że  \alpha będzie prawdziwe w następnym momencie (oznaczany też jako  \circ )
    •  G -  G \alpha oznacza, że  \alpha jest prawdziwe w każdym momencie (  G \alpha \equiv \alpha U \bot )
    •  F -  F \alpha oznacza, że  \alpha będzie prawdziwe w pewnym momencie w przyszłości (  F \alpha \equiv \top U \alpha    )
    •  F^{\infty} -  F^{\infty} \alpha oznacza, że  \alpha będzie prawdziwe w przyszłości w nieskończenie wielu momentach (zawsze z wyjątkiem pewnej skończonej liczby momentów) (  F^{\infty} \alpha \equiv GF \alpha   )
    •  G ^{\infty} -  G^{\infty} \alpha oznacza, że  \alpha będzie prawdziwe od pewnego momentu w przyszłości (  G^{\infty} \alpha \equiv FG \alpha   )
  • nawiasy

Formuły[edytuj | edytuj kod]

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

  • każde wyrażenie  \alpha \in WA jest formułą
  • jeśli \alpha i \beta są formułami, to \alpha \wedge \beta i \neg \alpha też są formułami
  • jeśli \alpha i \beta są formułami, to \alpha U \beta i  X \alpha też są formułami

Prawdziwość formuł[edytuj | edytuj kod]

  • Oznaczenia:

(M,x) \models \alpha - formuła \alpha jest prawdziwa w strukturze M na ścieżce x
 (M,s_{i}) \models \alpha - formuła \alpha jest prawdziwa w strukturze M w stanie s_{i}

  • warunki prawdziwości podstawowych formuł:

 (M,s_{i}) \models p \Leftrightarrow p \in L(s_{i})
(M,s_{i}) \models (\alpha \wedge \beta) \Leftrightarrow ((M,s_{i}) \models \alpha) \wedge ((M,s_{i}) \models \beta)
(M,s_{i}) \models \neg \alpha  \Leftrightarrow   \neg (M,s_{i}) \models \alpha
(M,s_{i}) \models \alpha U \beta \Leftrightarrow \exists_{k>i} (M,s_{k}) \models \beta \wedge (\forall j: (i \leq j  < k) \quad  (M,s_{j}) \models \alpha))
(M,s_{i}) \models X \alpha \Leftrightarrow (M,s_{i+1}) \models \alpha


PLTLFO[edytuj | edytuj kod]

Odmiana logiki LTL oparta o rachunek predykatów pierwszego rzędu.

Język[edytuj | edytuj kod]

  • wszystkie elementy PLTL
  • kwantyfikatory -  \forall , \exists
  • znak równości  =
  • symbole predykatywne  P, Q, R, \ldots
  • symbole funkcyjne  f, g, h, \ldots
  • symbole stałe  c_{1}, c_{2}, \ldots
  • zmienne  x_{1}, x_{2}, \ldots

Formuły[edytuj | edytuj kod]

  • termy:
    • zmienne,
    • stałe,
    • wyrażenia postaci:  f(t_{1}, t_{2}, \ldots, t_{n}) , gdzie   t_{i} są stałymi bądź zmiennymi
  • predykaty:
    • wyrażenia postaci:  P(t_{1}, t_{2}, \ldots, t_{n}) , gdzie  t_{i} są stałymi bądź zmiennymi
  • atomy:
    • stałe,
    • predykaty,
    • wyrażenia postaci:  t_{1}=t_{2} , gdzie  t_{1} i  t_{2} są stałymi bądź zmiennymi
  • formuły:
    • takie, jak w PLTL,
    • atomy,
    • wyrażenia postaci:  \forall x \ \alpha oraz  \exists x \  \alpha , gdzie  \alpha jest formułą, a  x jest zmienną.


Linki zewnętrzne[edytuj | edytuj kod]