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?

Improve this question
$\endgroup$
3
  • $\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, 2014 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$
    – Force444
    Oct 19, 2014 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, 2014 at 11:49

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
3
  • $\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$
    – Force444
    Oct 19, 2014 at 8:54
  • $\begingroup$ And based on what you said in your question, if the implication works both ways, then they are equivalent? $\endgroup$
    – Force444
    Oct 19, 2014 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, 2014 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.