Timeline for Counterexample for LTL - CTL equivalence
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 28, 2016 at 8:05 | comment | added | Pieter Verschaffelt | Oh ok, thank you very much! In that case I understand what happened. I indeed read the formula as $(EF AG p) \wedge AF q$. | |
| Jan 27, 2016 at 16:10 | comment | added | Shaull | Hmm. I read your CTL formula as $EF(AGp\wedge AFq)$, in which case my example is fine. But if it's intended as $(EFAGp)\wedge AFq$, then my answer is incorrect, and I think that there is no (non-empty) model that will have the desired property - obviously $AFq$ has to hold, by the LTL formula, and if $EFAGp$ doesn't hold, then along every path, every state has a path from it in which $AGp$ doesn't hold, which means we can construct a path that does not satisfy $FGp$. | |
| Jan 27, 2016 at 15:40 | vote | accept | Pieter Verschaffelt | ||
| Jan 27, 2016 at 14:08 | comment | added | Pieter Verschaffelt | I have one more little question: I don't quite understand why $AF q$ never holds? The computation starts with q, so at that point $AF q$ is satisfied? Or not? | |
| Jan 27, 2016 at 13:50 | comment | added | Pieter Verschaffelt | Thank you! I will practice more then :) Thank you for your help! | |
| Jan 27, 2016 at 13:33 | comment | added | Shaull | As with most problems, there is no "trick", just reasoning and some experience. Conceptually, it is possible to find such an example algorithmically: let $\phi$ be an LTL formula and $\psi$ be a CTL formula, then you can construct the CTL* formula $A\phi\wedge \neg \psi$, and then use CTL* satisfiabilityto find a model for the formula. But the complexity of this algorithm is terrible - 2EXPTIME, so it's not suited for solving exercises. | |
| Jan 27, 2016 at 12:58 | vote | accept | Pieter Verschaffelt | ||
| Jan 27, 2016 at 15:40 | |||||
| Jan 27, 2016 at 12:58 | comment | added | Pieter Verschaffelt | Thank you very much! :) I see now. Is there some trick that helps you find such differences between LTL and CTL or is it just plane reasoning? | |
| Jan 27, 2016 at 12:54 | history | answered | Shaull | CC BY-SA 3.0 |