Global model checking

Question

Professor I need few edge case clarification regarding global model checking

1. Existential predecessor or universal predecessor of all set is all set but the dead end states.

2. Existential predecessor  or universal predecessor of an empty set will include all the dead end states.

Is this statement true? If false please clarify this. And Can you please provide for existential or universal successor of all and empty set what it will add?

Answer 1

Some of your statements are true, some are not (see slide 56 of Chapter 4 on Transition systems):

for the empty state set, we get:

• pre∃({}) := {}
• pre∀({}) := {s ∈ S | suc(s) = {}} (deadend states)
• suc∃({}) := {}
• suc∀({}) := {s ∈ S | pre(s) = {}} (root states)

for the set of all states S, we get:

• pre∃(S) := {s ∈ S | suc(s) ̸= {}} (all except for deadends)
• pre∀(S) := S
• suc∃(S) := {s ∈ S | pre(s) ̸= {}} (all except for root states)
• suc∀(S) := S