# Difference between equivalence and implication

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?

• 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. Oct 19, 2014 at 11:38
• @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. Oct 19, 2014 at 11:43
• 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. Oct 19, 2014 at 11:49

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.
• 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. Oct 19, 2014 at 9:04