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 ?