Logica temporale lineare

Da Wikipedia, l'enciclopedia libera.

La logica temporale lineare o LTL (Linear Temporal Logic) è un'estensione della logica booleana che introduce il concetto di evoluzione nel tempo e può essere vista come:

  • una interpretazione di ogni percorso dei modelli di Kripke;
  • un modello lineare del tempo;
  • un insieme di operatori temporali.

Operatori[modifica | modifica wikitesto]

La logica temporale lineare LTL è composta da 3 operatori unari e 2 operatori binari:

  • X, "Next": Xα è vera nello stato st se e solo se α è vera nello stato successivo st+1;
  • F, "Future" (o "Eventually"): Fα è vera nello stato st se e solo se α è vera qualche stato successivo st' con t'≥t;
  • G, "Globally" (o "Henceforth"): Gα è vera nello stato st se e solo se α è vera in tutti gli stati successivi st' con t'≥t;
  • U, "Until": αUβ è vera in st se e solo se: β è vera in alcuni stati futuri st', con t'≥t; α è vera in tutti gli stati futuri st, con t'>t≥t.
  • R, "Release": αRβ è vera in st se e solo se: β è vera in tutti gli stati futuri st', con t'≥t; α è vera in alcuni stati futuri st, con t'>t≥t.

Gli operatori temporali hanno la priorità sugli operatori booleani.

Semantica[modifica | modifica wikitesto]

La semantica formale degli operatori temporali è così definita:

  • \pi,s_i \models \neg \alpha \iff \pi,s_i \not\models \alpha
  • \pi,s_i \models \alpha \and \beta \iff \pi,s_i \models \alpha\  \and \ \pi,s_i \models \beta
  • \pi,s_i \models X\alpha \iff \pi,s_{i+1} \models \alpha
  • \pi,s_i \models F\alpha \iff \exists j\ge i\ : \ \pi,s_j \models \alpha
  • \pi,s_i \models G\alpha \iff \forall j\ge i\ : \ \pi,s_j \models \alpha
  • \pi,s_i \models \alpha U \beta \iff  \exists j\ge i\ : \ \pi,s_j \models \beta \ \mbox{ e} \ \forall k \ \mbox{tale che} \ i\le k \le j\ : \ \pi,s_k \models \alpha
  • \pi,s_i \models \alpha R \beta \iff  \forall j\ge i\ : \ \pi,s_j \models \beta \ \mbox{ e} \ \exists k \ \mbox{tale che} \ i\le k \le j\ : \ \pi,s_k \models \alpha

Dove \pi è un percorso del modello di Kripke e s_i è lo stato corente. \alpha , \beta sono formule booleane.

Proprietà Sintattiche[modifica | modifica wikitesto]

Date α e β formule LTL, allora:

  • F\alpha \iff \top U\alpha
  • G\alpha \iff \bot R\alpha
  • F\alpha \iff \neg G \neg \alpha
  • G\alpha \iff \neg F \neg \alpha
  • \neg X\alpha \iff X \neg \alpha
  • \alpha R\beta \iff \neg(\neg \alpha U \neg \beta)

Da queste ugualianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli \neg, \ X, \ U.

Regole[modifica | modifica wikitesto]

Date α e β formule LTL, allora:

  • F \alpha \Leftrightarrow (\alpha \lor XF \alpha);
  • G \alpha \Leftrightarrow (\alpha \land XG \alpha);
  • \alpha \cup \beta \Leftrightarrow(\beta \lor (\alpha \land X (\alpha \cup \beta)));

Logica LTL e proprietà dei Modelli di Kripke[modifica | modifica wikitesto]

La logica LTL rispetta le proprietà di Safety, Liveness, Fairness e Strong Fairness proprie dei Modelli di Kripke:

  • Safety: "Non succederà mai che all'arrivo del treno la sbarra sia alzata", ovvero: G(!(arrivo_treno∧sbarra_alzata));
  • Liveness: "Se c'è un input, allora in futuro ci sarà un output", cioè: G(input→Foutput);
  • Fairness: "Invio infinitamente spesso un messaggio", cioè: GFinvio;
  • Strong Fairness: "Se invio infinitamente spesso, allora riceverò infinitamente spesso", ovvero: GFinvio→GFricevo.

Voci correlate[modifica | modifica wikitesto]

Collegamenti esterni[modifica | modifica wikitesto]