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


524 users

0 votes

I thought for existential successor, we rename the variables (p,q) to (p', q') and vice versa. But for this solution, that is not the case. Also, isn't there supposed to be a separator for solving when p' = 0 and p' = 1?. 

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

1 Answer

0 votes
No, the variables are not renamed "vice versa", why do you think so? You can find the symbolic computation of successors and predecessors on page 68 of the chapter on transition systems. The existential successors are computed by first computing the existential quantification on all current variables of the conjunction of the transition relation and the state set, and since that is a formula in the next variables, these are replaced then with the corresponding current variables.

I have no idea what you mean with a separator? Do you mean quantifier or do you mean cofactors?
by (165k points)
Thank you. But in one of the exercise solution pdf, it was written that "In successor we rename (p, q, a) to (p′, q′, a′) and vice-versa ".

Example solved in the solution sheet of the exercise
Let each state in the Kripke structure be described by the variables {p, q, a, o}.
Let the transition relation R be described by ψR = (p′ ↔ q) ∨ a. Let the set Q be described by φQ = ¬p
suc∀R(Q) = {s2 | ∀s1(s1,s2) ∈ R → s1 ∈ Q}
suc∀R(Q) = ∀p′,q′,a′ [(p ↔ q′) ∨ a′) → ¬p′]
(In successor we rename (p, q, a) to (p′, q′, a′) and vice-versa )
 =[1]p′=0 ∧[¬((p↔q′)∨a′)]p′=1
=[¬((¬p)∨a′)]q′=0 ∧[¬((p)∨a′)]q′=1
= [1]a′=0 ∧ [0]a′=1
= 0/ false
Note:For universal ∀, the separator is ∧

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 24, 2023 in # Study-Organisation (Master) by yk (2.7k points)
Imprint | Privacy Policy