0
$\begingroup$

In terms of CTL formulae, what is the difference between equivalence and implication?

(prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds")

E.g. AG (prop1 && prop2) versus (AG prop1) && (AG prop2)

Are those two formulae related by implication i.e. the left hand side implies the right hand side? Or are they actually equivalent?

$\endgroup$
  • $\begingroup$ What is CTL ? New acronyms crop up all the time, sometimes ambiguously, and it is usually nice to remind the meaning at the first use, since readers have very different backgrounds. $\endgroup$ – babou Oct 19 '14 at 11:38
  • $\begingroup$ @babou I apologise. It stands for Computation Tree Logic and is a branching time logic. Used for e.g. software verification techniques such as model checking to reason about properties of a model in terms of a transition system. Probably not the best definition but hope it narrows it down. $\endgroup$ – DSF Oct 19 '14 at 11:43
  • 1
    $\begingroup$ Thanks. No need to apologize ... I had the comment for everyone to read, as it is a common problem. It just fell on you (sorry). And thanks for all the details. $\endgroup$ – babou Oct 19 '14 at 11:49
3
$\begingroup$

First, to answer the question in your question title: the difference between equivalence and implication in CTL formulae is the same as the difference between equivalence and implication in propositional logic, that is, $A \leftrightarrow B$ is the same $(A \to B) \land (B \to A)$.

But your real question is whether $\mathrm{AG}\,(A \land B)$ is equivalent to $\mathrm{AG} \,A \land \mathrm{AG}\,B$. To solve this question, you have to look at the semantics of the operators AG and $\land$; that is, what do $\mathrm{AG}\,\phi$ and $\psi_1\land\psi_2$ mean (for arbitrary formulas $\phi,\psi_1,\psi_2$?

The semantics of CTL works via transition systems. Two formula are equivalent if they are true in exactly the same transition systems and states. Looking at the semantics of AG and $\land$, it should be fairly easy to decide whether there is a transition system where the one formula is true and the other isn't.

$\endgroup$
  • $\begingroup$ Thank you. I did try to come up with a transition system where the above would not result in the same states being true, but I can't. So my conclusion is that they are equivalent. Just to confirm my understanding, say we changed it a bit so swapping all AG with EF instead. Now they're not equivalent because I can come up with a transition system where one holds for some state where the other formula doesn't hold. But one could imply the other? Am I right to say that if one formula is true and then only because of that the other is also true then we have implication? $\endgroup$ – DSF Oct 19 '14 at 8:54
  • $\begingroup$ And based on what you said in your question, if the implication works both ways, then they are equivalent? $\endgroup$ – DSF Oct 19 '14 at 8:55
  • 1
    $\begingroup$ Yes, if A follows from B and B follows from A then, by definition, A and B are equivalent. And indeed, $\mathrm{EF}\,(A \land B)$ and $\mathrm{EF}\,A \land \mathrm{EF}\,B$ are not equivalent, but the first does imply the second. $\endgroup$ – Hoopje Oct 19 '14 at 9:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.