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 ?