|
Buongiorno a tutti, per motivi accademici mi trovo a studiare LTL E CTL model checking, mi sono trovato a dover svolgere un esercizio in cui mi si chiede se due formule CTL sono equivalenti oppure no, nel caso non lo fossero devo fare in modo di illustrare un percorso tramite automa di kripke che rende vera una delle due formule e falsa l'altra.
Le formule dell'esercizio sono le seguenti:
EF (p or q) = EF(p) or EF(q) ?
AF(p or q) = AF(p) or AF(q) ?
A(p U ( A(q U r) )) = A(A(p U q) U r) ?
Per quanto riguarda le prime due formule, ragionando un pochino e facendo un po' di prove sono arrivato alla conclusione che siano uguali. (Se ho sbagliato vi prego correggetemi)
Per quando riguarda la terza invece sono un pochino disorientato sapreste mica aiutarmi?
Conoscete un modo per verificare l'uguaglianza senza sbagliare?
Vi ringrazio in anticipo per il vostro aiuto.
| 
