Logica temporale lineare

Da Wikipedia, l'enciclopedia libera.

La logica temporale lineare o LTL (Linear Temporal Logic) è:

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

Gli operatori temporali della logica LTL sono:

  • 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.

Regole[modifica | modifica wikitesto]

Date α e β formule LTL, allora:

  • F \alpha \Leftrightarrow (\alpha \lor XF \alpha);
  • G \alpha \Leftrightarrow (\alpha \lor 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.