CTL exam question

Question

I am solving exam question : 17.02.2021 : Q. 7 (c) 2021.02.17.vrs.solutions.pdf (uni-kl.de)

I am trying to satisfy S1 and not S2.

My Solution:.

I am verifying the correctness using the tool ModelChecking.html 

Input :

vars a,b;

init 0;

labels 0:a; 1:;

transitions 0->0;

For S1 tool says Property E [(E F a) WU b] holds in states {s0} ⊇ {s0} = k.init. Hence, the structure satisfies the property.

For S2 tool says Property b | E F a & E X b | E F (b & E F a) holds in states {} ⊉ {s0} = k.init. Hence, the structure does not satisfy the property. 

Q1. Does the above checking is correct or it is not a correct way to verify CTL satisfiability ?

Q2. Is there any way to verify CTL* formula using tool as well ?

Answer 1

The above checking of the CTL formulas is correct. For CTL*, there is currently no tool available.

Comments

Thank you for this answer.

Would it be possible for you to suggest an external CTL* tool for this ?