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

557 users

0 votes

Hi, 

I have one issue regarding the following Kripkee solution. Can you please explain to me how is this not satisfying [[a SB b] SB c and satisfying [a SB [b SB c]].

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

1 Answer

+1 vote
 
Best answer

Clearly, the path of the Kripke structure always satisfies a,b, and c. It is therefore never the case that b holds before c, and therefore [b SB c] is always false. Same way, it is never the case that a holds before b, and therefore [a SB b] is always false. Thus, we may now consider the formulas

  • [a SB false]
  • [false SB c]

The first formula is obviously true, since (for example) at the first point of time, "a" holds, and that holds before "false" becomes true (which is never the case). The second formula is however false, since false cannot become true, but it should, and it should even become true before c holds, but that is already true at the initial point of time.

 

by (170k points)
selected by

Related questions

0 votes
1 answer
asked Jan 23, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
2 answers
0 votes
2 answers
asked Jan 25, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
Imprint | Privacy Policy
...