0 votes
Hello

Please may elaborate "Problem 7.a" in below exam?

https://es.cs.uni-kl.de/teaching/vrs/exams/2021.02.17.vrs/2021.02.17.vrs.solutions.pdf

Thanks.
in * TF "Intelligent Systems" by (770 points)

1 Answer

0 votes

You can try the model checker in the teaching tools with the following transition system

    vars b,c;
    init 0;
    labels 0:c; 1:; 2:b;
    transitions 0->1; 1->2; 2->2;

and properties

c ∧ E X(b∧¬c);
c ∧ E X E F(b∧¬c);

You will then see that

  •     〖b〗= {s2}
  •     〖c〗= {s0}
  •     〖!c〗= {s1;s2}
  •     〖b & !c〗 = {s2}
  •     〖EX(b & !c)〗 = {s1;s2}
  •     〖c & EX(b & !c)〗 = {}
  •     〖EF(b & !c)〗 = {s0;s1;s2}
  •     〖EX EF (b & !c)〗 = {s0;s1;s2}
  •     〖c & EX EF (b & !c)〗 = {s0}

The latter is clear since c holds on s0, and s0 has a next state, namely s1, such that EF(b & !c) holds there. Note that b & !c holds on s2, and that s2 can be reached from s0;s1;s2.

by (92.2k points)

Related questions

0 votes
1 answer
asked Aug 24, 2020 in * TF "Emb. Sys. and Rob." by nikita (300 points)
0 votes
1 answer
asked Aug 23, 2020 in * TF "Emb. Sys. and Rob." by ssripa (550 points)
0 votes
1 answer
asked Aug 20, 2020 in * TF "Emb. Sys. and Rob." by nikita (300 points)
0 votes
1 answer
asked Aug 20, 2020 in * TF "Emb. Sys. and Rob." by maherin (370 points)
0 votes
1 answer
asked Aug 17, 2020 in # Study-Organisation (Master) by RS (770 points)
Imprint | Privacy Policy
...