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

870 questions

988 answers


439 users

0 votes

I have one doubt here 

Why A[a SB true] gives state set {s8} ?

In SB both RHS and LHS cannot coexist means they can't both be true, so here why s8 is included when a is true and other term is always true? 
Is it because of Universal Path quantifier because it considers deadend state as well so thatswhy it is there ?

Tool Solution :

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

2 Answers

+1 vote

That S8 is in the state set has nothing to do with SB but with A. Since S8 has no infinite paths, it satisfies a condition requiring all paths to satisfy the unsatisfiable condition.

You are right about the following assumptions:

  1. [ whatever SB true ] is satisfied by no path
  2. Precisely the deadend states satisfy A false
by (25.2k points)
Thanks for this explanation.
+1 vote
This is because s8 is a deadend state. Note that deadend states satisfy all formulas A psi no matter what psi is (even A false is satisfied this way).
by (139k points)
Thanks for this explanation.

Related questions

Imprint | Privacy Policy