If I have two CTL equations, how do I prove they're equivalent or that one implies the other?
What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the equivalence of the two or an implication
$\begingroup$
$\endgroup$
1
-
$\begingroup$ You could use a proof system (e.g. Pnueli & Kesten's paper in CONCUR 2002 for the richer CTL${}^*$) or ask a model checker such as nuSMV. $\endgroup$– KaiCommented Nov 27, 2023 at 6:11
Add a comment
|