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

912 questions

1k answers

1.4k comments

441 users

0 votes

Hi,

Given a Kripke structure K={V,φI,φR}K={V,φI,φR}
where V={a,b,c}V={a,b,c}φI=φI=!(b<->a), φR=φR=next(a)&a&(b|b<->next(c)).

the task is: "Compute the set of states from which the states satisfy !b can be reached symbolically, and submit the solution in disjunctive normal form."

As I understand the question, the task is to compute the existential predecessors of !b, which would result in the following:

∃next(a).∃next(b).∃next(c).next(a)&a&(b|b<->next(c))&!next(b)
  = ∃next(b).∃next(c).!next(b)&a&(b<->next(c))
  = ∃next(c).a&(b<->next(c))
  = a&b|a&!b

However, neither   a&b&c|a&b&!c|a&!b&c|a&!b&!c   nor   a   is accepted as a solution. 
Do I understand something about the question wrong?

closed with the note: Answered
in * TF "Emb. Sys. and Rob." by (350 points)
closed by

1 Answer

+1 vote
 
Best answer
We are looking for the states from which the specified state set can be reached in a arbitrary number of steps. You calculated the states from where the set can be reached in precisely one step (existential predecessors).

The required set can be obtained by starting with the specified set (reached in zero steps), and adding (by the means of a disjunction) its existential predecessors. The step of adding predecessors is then continued until fixpoint.
by (25.6k points)
selected by

Related questions

Imprint | Privacy Policy
...