LTL

Sissejuhatus

Iga Boole'i muutuja on LTL valem. LTL abil saab väljendada süsteemi järgnevaid omadusi:

  • Reachability, et praegusest olekust jõuab soovitud olekuni
  • Turvalisus (safety), halb omadus ei saa kunagi rahuldatud
  • Liveness, hea omadus rahuldatakse mõnes tuleviku olekus
  • Deadlock freedom, tupikolekuni ei jõuta kunagi

Deadlock, A ootab B järgi ning B ootab A järgi. Un-fairness, A ootab B järgi kuid B töötab õigesti aga ei anna kunagi järge A kätte. Näiteks: ristmikul auto saab kunagi paremale pöörata.

Süntaks

Temporaal-loogikas LTL ehk Linear Time Logic vaatleb ühte teed. Öeldakse, et LTL valem φ kehtib mudelis M alates olekust S[j]:

\begin{equation*} (M, S_j) \models \varphi \end{equation*}

Samamoodi saab öelda, et φ ei kehti mudelis M alates olekust S[j]:

\begin{equation*} (M, S_j) \not\models \varphi \end{equation*}

LTL valem on defineeritud kui:

\begin{equation*} \varphi ::= \bot | \top | p | (\neg \varphi) | (\varphi \land \varphi) | (\varphi \lor \varphi) | (\varphi \implies \varphi) | X\varphi | F\varphi | G\varphi | \psi U \varphi | \psi W \varphi \end{equation*}

neXt operaator

Omadus φ peab kehtima järgmises olekus (next):

\begin{equation*} (M, S_j) \models X \varphi \Leftrightarrow (M, S_{j+1}) \models \varphi \end{equation*}

Operaatori võib kirjutada ka kui:

\begin{equation*} X \varphi \equiv \circ \varphi \end{equation*}

Future operaator

Omadus φ peab kehtima mõnes tuleviku olekus:

\begin{equation*} (M, S_j) \models F \varphi \Leftrightarrow \exists k, k >= j, (M, S_k) \models \varphi \end{equation*}

Operaatori võib kirjutada ka kui:

\begin{equation*} \diamond \varphi \equiv F \varphi \end{equation*}

Näide: Ma olen kunagi õnnelik.

Global operaator

Omadus φ peab kehtima kõigis tuleviku olekutes:

\begin{equation*} (M, S_j) \models G \varphi \Leftrightarrow \forall k, k >= j, (M,S_k) \models \varphi \end{equation*}

Operaatori võib kirjutada ka kui:

\begin{equation*} \square \varphi \equiv G \varphi \end{equation*}

Näide: Ma olen alati õnnelik.

Until operaator

Omadus φ kehtib lõpuks, kuni seni kehtib ψ kõigis olekutes (until):

\begin{equation*} \psi \cup \varphi \equiv \psi U \varphi \end{equation*}

Näide: Ma olen õnnelik kuni ma teen midagi valesti.

Näide

Alati kui auto pidurile vajutada siis lõpuks jääb auto seisma:

\begin{equation*} \square (break \rightarrow \diamond stop ) \end{equation*}

P kehtib järgmises või ülejärgmises olekus:

\begin{equation*} X p \lor X X p \end{equation*}
Kommunikeerivad järjestikprotsessid Formaalne verifitseerimine Lauseloogika First-order logic Ajastatud automaadid
QAoES TU Berlin