# Universal Predecessor

I have a question regarding this example from the exercise lesson (page 5):

Shouldn't S0 as well as S3 also be part of the universal predecessors of (S3,S4) since all outgoing transitions from S0 and S3 lead to (S3,S4)?

+1 vote

I have added two additional variables p,q to uniquely identify the states so that I have the following Kripke structure:

```vars a,b,d,p,q;
init 1;
labels
0:b,d;   1:a;   2:b,d,p;
3:b,d,q; 4:a,q; 5:b,d,p,q;
transitions
1->0; 1->2; 1->3; 2->2; 3->4; 4->2; 4->3; 4->5; ```

which looks as follows:

Using our model checker, it computed the universal predecessors of s3,s4, i.e.

`    [](!a&b&d&!p&q | a&!b&!d&!p&q)`
```as follows:
〖!a & b & d & !p & q〗 = {s3}
〖a & !b & !d & !p & q〗 = {s4}
〖!a & b & d & !p & q | a & !b & !d & !p & q〗 = {s3;s4}
〖[] (!a & b & d & !p & q | a & !b & !d & !p & q)〗 = {s0;s3;s5}
```

Hence, pre∀({s3,s4}) = {s0,s3,s5}.

The universal successors of {s3,s4} are computed as follows:

```  〖!a & b & d & !p & q〗 = {s3}
〖a & !b & !d & !p & q〗 = {s4}
〖!a & b & d & !p & q | a & !b & !d & !p & q〗 = {s3;s4}
〖[:] (!a & b & d & !p & q | a & !b & !d & !p & q)〗 = {s1;s4;s5}
```

Hence, suc∀({s3,s4}) = {s1,s4,s5}.

Without the dashed transition, I also computed pre∀({s3,s4}) = {s0,s3,s5} and suc∀({s3,s4}) = {s1,s4,s5}.

by (142k points)
edited by
Thank you. Therefore I assume the presentation to be wrong.

I think you only made one typo, namely "Hence, pre∀({s3,s4}) = {s0,s3,s4}."
However, you computed [] (!a & b & d & !p & q | a & !b & !d & !p & q)〗 = {s0;s3;s5}
Yes, you are right! I have fixed it now.
+1 vote

According to my notes from the Exercise session the universal predecessors are {s0,s3,s5}.

This should be a mistake in the Exercise slides.

Greetings

Mario

by (230 points)