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

1.1k questions

1.2k answers

1.6k comments

546 users

0 votes

Exam Problem : 29.08.2017 : Q 8 e : 2017.08.29.vrs.solutions.pdf (uni-kl.de)

Problem :

My Solution :

I thought it like below to satisfy S1 and not S2:

X !a holds in {s0, s1, s2}

!a holds in {s0, s2} 

!a & X !a holds in {s0, s2} 

AF (!a & X !a) holds in {s0, s2} 

Hence it satisfies S1.

X !a holds in {s0, s1, s2}

AX !a holds in {s1, s2}

!a & AX !a holds in {s2} 

AF (!a & AX !a) holds in {s1, s2} => (There is path in s0 in which it can loop forever and never reach s2)

No initial set, hence not satisfied.

Q1. Could you please let me know if my Kripke Structure is correct ?

Q2. Could you please let me know if my way of proofing is correct ?

Thanks in advance

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

1 Answer

0 votes
Your Kripke structure and your arguments are fine, but your proof is now well presented. You should not say that a path formula like X!a holds in {s0, s1, s2} since path formulas hold on paths.

For S1, you should rather argument about the two paths s0^omega nd s0^*.s1.s2^omega leaving s0, both satisfy !a&X!a. For the other formula, which is a CTL formula, state-based reasing is appropriate.
by (166k points)

Related questions

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