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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

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 ?

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

1 Answer

0 votes
The above checking of the CTL formulas is correct. For CTL*, there is currently no tool available.
by (170k points)
Thank you for this answer.

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

Related questions

0 votes
1 answer
0 votes
1 answer
asked Aug 3, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...