8
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Vijay D
    Mar 22, 2012 at 8:35
  • $\begingroup$ @VijayD: $Sat_{TS}$ is the set of states of TS for which starting at one of that states satisfies the formula. $\endgroup$
    – bitmask
    Mar 22, 2012 at 10:31

4 Answers 4

Reset to default
6
$\begingroup$

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".

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – bitmask
    Mar 21, 2012 at 21:53
  • $\begingroup$ Why not just write "Check whether $\neg(\Phi\equiv\Psi)$ is satisfiable."? $\endgroup$
    – Dave Clarke
    Mar 22, 2012 at 10:19
  • $\begingroup$ @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? $\endgroup$
    – jmad
    Mar 22, 2012 at 10:33
  • $\begingroup$ 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? $\endgroup$
    – Dave Clarke
    Mar 22, 2012 at 10:37
3
$\begingroup$

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.

Improve this answer
$\endgroup$
0
$\begingroup$

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.

Improve this answer
$\endgroup$
-1
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • 3
    $\begingroup$ Is this a comment/request or an answer? $\endgroup$
    – A.Schulz
    Nov 25, 2012 at 8:13
  • $\begingroup$ 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? $\endgroup$
    – Rohit
    Nov 28, 2012 at 1:20
  • $\begingroup$ Then your remark qualifies as a comment. Please post it as a comment and delete your "answer". $\endgroup$
    – A.Schulz
    Nov 28, 2012 at 6:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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