Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

870 questions

988 answers


439 users

0 votes

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 ?

in * TF "Emb. Sys. and Rob." by (2.9k points)

1 Answer

0 votes
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).
by (139k points)
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 ?

Related questions

Imprint | Privacy Policy