# How can I decide manually whether two CTL formulae are equivalent?

Assume I have two formulae $\Phi$ and $\Psi$ (over the same set of atomic propositions $AP$) in CTL. We have that $\Phi \equiv \Psi$ iff $Sat_{TS}(\Phi) = Sat_{TS}(\Psi)$ for all transition systems $TS$ over $AP$.

Given that there are infinitely many transition systems, it's impossible to check them all. I thought about using PNF (Positive Normal Form, allowing negation only next to literals) because judging from its name it should give me the same formula for $\Phi$ as for $\Psi$ iff they are equivalent, but I'm not convinced this works in all cases (you could say, I'm not convinced PNF is actually a normal form).

For example, take $\forall \mathrm{O} \forall \lozenge \Phi_0 \stackrel{?}{\equiv} \forall \lozenge \forall \mathrm{O} \Phi_0$ (where $\mathrm{O}$ is the next operator and $\lozenge$ is the eventually operator). I'm looking for a way do do this by hand.

-
What is $Sat_{TS}$? The formula satisfies the transition system? I assume your definition of a transition system includes an initial state then and the formula is checked at this state. – Vijay D Mar 22 '12 at 8:35
@VijayD: $Sat_{TS}$ is the set of states of TS for which starting at one of that states satisfies the formula. – bitmask Mar 22 '12 at 10:31

It seems to me that "$\Phi≡\Psi$" is equivalent to "Neither $(\Phi ∧ ¬\Psi)$ nor $(\Psi ∧ ¬\Phi)$ is satisfiable".

Therefore deciding equivalence is as difficult as deciding satisfiability, since "$\Phi$ satisfiable" is equivalent to "not ($¬\Phi≡\top$)".

In this article there is a mention of a an exponential procedure to decide satisfiability in CTL, so it should be enough to run the algorithm on the two formulas I wrote above.

PS: I am not at all an expert in this field, so please check what I wrote. If this makes sense, I will remove the various "seems" and "should".

-
I don't know if this is correct (something doesn't seem right, can't put my finger on it, though), but I believe there is an easier way of doing this. – bitmask Mar 21 '12 at 21:53
Why not just write "Check whether $\neg(\Phi\equiv\Psi)$ is satisfiable."? – Dave Clarke Mar 22 '12 at 10:19
@DaveClarke: he defines $≡$ with a quantification over all LTS, so $≡$ is not in the grammar. However $¬(\Phi\Leftrightarrow\Psi)$ seems good. Do you think it's better? I find my formulation makes the reader feel the difference between syntax and semantics, but who am I to judge? – jmad Mar 22 '12 at 10:33
The paper you cited uses $\equiv$ instead of the usual $\Leftrightarrow$, which is why I used that symbol. It just seemed more direct than your statement, but who am I to judge? – Dave Clarke Mar 22 '12 at 10:37

If you want to prove the identities by hand, I do not know if there are absolutely general techniques. You can start with the axioms and well known identities for CTL and work from there.

If you want the answer and worry about having a human readable proof separately, you can use a CTL satisfiability checker like MLSolver.

-

Your example is not equivalence assume a transition system by two state which all of them are initial, and there is a loop in state which satisfy \phi. To prove equivalence of two CTL formula you should use definition of semantics.

-

Could you express this in the fixpoint characterization for CTL formulas? That might help you prove their equivalence. http://www-2.cs.cmu.edu/~modelcheck/ed-papers/VTfFSCS.pdf

-
Is this a comment/request or an answer? – A.Schulz Nov 25 '12 at 8:13
Well I dont know of a standard proof technique for proving equivalence. So it's meant to be a question to the community. Could we use the fixpoint characterization to prove equivalence? – Rohit Nov 28 '12 at 1:20
Then your remark qualifies as a comment. Please post it as a comment and delete your "answer". – A.Schulz Nov 28 '12 at 6:17