How to check if two CTL/LTL formula are equivalent using tool

Question

1. CTL Tool : CTL_Tool

2. LTL Tool : LTL_Tool

Could you please let me know how can I correctly verify if two CTL or two LTL formulae are equivalent using tools ?

Answer 1

For CTL, there is only a model-checking tool, no tool for proving validity or satisfiability. For LTL, both problems are the same and the mentioned tool above can do both in that sense (but it has been implemented for validity proving).

Comments

I understood your point. Thanks for clarifying.

Could there be multiple output of translation between different logics ? For e.g. from CTL* to CTL or LTL the result could be non-deterministic ?