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

1.1k questions

1.2k answers

1.6k comments

529 users

0 votes
Consider the following symbolic representation of a Kripke Structure K = (V, ΨI, ΨR) over variables V = {p, q} and the following initial states ΨI and transition relation ΨR: V = {p, q} ΨI = ¬q ΨR = (p → (¬(p 0 ↔ q 0 ) ∨ (q 0 ↔ q)))

Construct the state transition diagram of K ? can someone help me out this?
in * TF "Emb. Sys. and Rob." by (200 points)

1 Answer

0 votes

Symbolic representations have been introduced on slide 53 of the lecture notes.

Here, your variables are V = {p, q}. Your initial states Are described by ΨI = ¬q. You transition relation is defined by  ΨR = (p → (¬(p' ↔ q') ∨ (q' ↔ q))). You'd do the following steps:

  1. Create all possible states. The variables p and q can either be present or absent. These yields four states: {}, {q}, {p}, {p,q}
  2. Marks the initial states. Those are the states satisfying ¬q. That means that q may not be present in the label. That's the case for {}, {p}.
  3. Find all satisfying assignments of the formula representing the transition relation. One satisfying assignment is p = q = q' = true, p' = false. The primed variables mark the destination, the unprimed ones the source of the source of the transition. This satisfying assignment corresponds to the transition {p, q} → {q}

I hope that helps. I am not quite sure at which point you got stuck when asking this question. The question is an exam question (Feb 2020, Page 8, Problem 3). You might have a look at the standard solutions to this and other exam questions. That might help understanding what is going on here.

In this solution, you can find a partial truth table. This means that for the unprimed variables, all combinations were plugged in and the formula was partially evaluated. For example p = q = 1 evaluated to p' ∨ q'. Every satisfying assignment to p', q' extends the partial assignment to a variable assignment that corresponds to a transition. A special case is the first line of the (partial) truth table. Here, the partial assignment p = q = 0 turned the whole formula true. This means that the transitions from {} (both p, q are false) lead to all states in the structure.

by (25.6k points)
edited by
i'm not sure how to find all satisfying assignments of the formula using truth table can yo plz help me with that
Basically, you just plug in all assignments and see whether it is satisfying. I added a paragraph about that.
Imprint | Privacy Policy
...