Sistemi di transizione che soddisfano LTL ma non CTL e viceversa

Question

Sto imparando la logica temporale e i sistemi di controllo del modello. Un esercizio concettuale con cui sto lottando è come creare un sistema di transizione che soddisfa solo uno di due proprietà date, quando una è in LTL e una è in CTL. Per esempio:

• Trova un sistema di transizione che soddisfi solo una delle seguenti due proprietà: $ FGP $, $ afegp $
• Trova un sistema di transizione che soddisfi solo una delle seguenti due proprietà: $ FGP $, $ EFEGP $
• Trova un sistema di transizione che soddisfi solo una delle seguenti due proprietà: $ GFP $, $ AGEFP $

Come dovrei iniziare quando provo a ragionare su questi tipi di problemi? In generale, è più facile progettare sistemi di transizione per proprietà LTL o proprietà CTL? O dipende dalla situazione?

Qualsiasi intuizione sarebbe apprezzata!