Questo sito utilizza cookies, anche di terze parti, per mostrare pubblicità e servizi in linea con il tuo account. Leggi l'informativa sui cookies.
Username: Password: oppure
Algoritmi - Formule equivalenti in CTL model checking
Forum - Algoritmi - Formule equivalenti in CTL model checking

Avatar
macco_cl (Normal User)
Rookie


Messaggi: 34
Iscritto: 27/02/2007

Segnala al moderatore
Postato alle 17:18
Mercoledì, 16/09/2015
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.

PM Quote