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

538 users

0 votes
In a Kripke structure K1 , if we have state s0 with {a} and a state s1 with {d} and in Kripke structure K2, if we have state q0 with {a,b,d} and another state {a,d}, in step so, do we take pairs of all these states like :

step0; {s0, q0}, {s0,q1} , {s1, q0 ), (s1,q1)

Or do we take state pairs with exactly the same value ?
in # Study-Organisation (Master) by (300 points)

2 Answers

0 votes
Hey,

As can be seen in chapter 4 (Transition Systems) on page 17, the following pairs of states are checked:  (s1 , s2 ) ∈ σ implies L1 (s1 ) ∩ V2 = L2 (s2 ) ∩ V1

For your example you have to check which set of variables is given for the Kripke structures.

Assume you have the variable set {a,d} given for K1 and {a,b.d} given for K2, this would mean that there is no state pair matching this property.
by (440 points)
0 votes

We take pairs of states with exactly the same observable label. Observable means that you  first have to remove all variables of a structure that are not know by the other structure and vice versa. After that the labels must be exactly the same for generating the pairs of step 0.

by (166k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 16, 2020 in * TF "Emb. Sys. and Rob." by nikita (300 points)
Imprint | Privacy Policy
...