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 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.6k 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 (170k points)
Thanks for this explanation.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...