Negazione della semantica dell'operatore fino a LTL

Question

Ho esaminato l'operatore fino all'operatore e l'operatore di rilascio e quando introdotto all'operatore di rilascio è stato suggerito che è equivalente a:

$ phi r psi equiv neg ( neg phi u neg psi) $

Ma quando si tenta di ottenere dalla definizione semantica dell'operatore fino alla definizione semantica dell'operatore di rilascio per negazione, rimango bloccato a metà. In particolare, rimango bloccato nel tentativo di negare a $ forall j <i $ espressione come mostrerò di seguito.

Quindi la definizione semantica di fino a:

$ pi modelli phi u psi iff esiste i geq0, pi [i] modelli psi land forall j leq i-1, pi [j] modelli phi $

Mettere le negazioni in:

$ pi modelli neg ( neg phi u neg psi) iff neg ( esiste i geq0, pi [i] modelli neg psi land forall j <i, pi, pi [j] modelli neg phi) $

$ iff forall i geq 0, neg ( pi [i] modelli neg psi) lor neg ( forall j <i, pi [j] modelli neg phi) $

$ iff forall i geq 0, ( pi [i] modelli psi) lor ( esiste j <i, pi [j] modelli phi) $

A parole, sto finendo con a livello globale $ psi $ o a livello globale esiste sempre un predecessore che soddisfa $ phi $. Che non può essere corretto come $ pi [j] $ non è definito quando $ i = 0 $.

La definizione semantica per l'operatore di rilascio a cui miravo è:

$ pi modelli phi r psi iff ( esiste i geq 0, pi [i] modelli phi land forall j leq i, pi [j] modelli psi) lor ( forall k geq 0, pi [k] modelli psi) $

Quindi ho parte dell'espressione corretta ($ forall k geq 0, pi [k] modelli psi equiv forall i geq 0, ( pi [i] modelli psi) $), ma sono davvero sconcertato da come ottenere la seconda parte o dove ho sbagliato.

Qualsiasi aiuto che mi illumina è molto apprezzato!

Grazie!