Kripke structure to satisfy S1&!S2 or S2&!S1

Question

Is there a way to check my solution using the tool for CTL*? 

The LTL tool where I can check S1->(my solution) is giving parse error for CTL* formula

Answer 1

Well, CTL* is not LTL, so that the LTL tool cannot handle CTL* formulas. However, for structures that have no branching, i.e., where every state has only one successor state, the CTL* and LTL formulas coincide. For the above, that is however not the case. So, there is no tool support for that kind of question as of now. It is also not planned at the moment.

Comments

Alright! Thank you.