how to compute the universal predecessor?

Question

can someone please explain the definition of  existential predecessor successor, universal predecessor and successor

Answer 1

Considering a state transition system with transition relation R, we can define the predecessors and successors for a single state s as follows:

• pre(s2) := {s1∈S | (s1,s2)∈R}
• suc(s1) := {s2∈S | (s1,s2)∈R}

Hence, pre(s2) are the states s1∈S that have a transition (s1,s2)∈R to s2, and suc(s1) are the states s2∈S that have a transition (s1,s2)∈R from s1. 

Extending the above functions to sets of states is more difficult. For example, we have to specify for pre(Q2) whether all successors of states s1 in question should be in Q2 or just some of them. This leads to the following definitions:

• pre∃(Q2) := {s1 ∈ S | suc(s1) ∩ Q2≠{}} 
• pre∀(Q2) := {s1 ∈ S | suc(s1) ⊆ Q2} 
• suc∃(Q1) := {s2 ∈ S | pre(s2) ∩ Q1≠{}} 
• suc∀(Q1) := {s2 ∈ S | pre(s2) ⊆ Q1}

Note that suc(s1) ⊆ Q2 means that all successors of s1 are contained in Q2, while suc(s1) ∩ Q2≠{} means that at least one successor of s1 must be inside Q2. 

Caution: There is the special case where a state s1 has no successors, i.e., suc(s1)={}. In that case, suc(s1) ∩ Q2 = {} ∩ Q2 = {}, and therefore s1 cannot be in a pre∃(Q2), but it is contained in every pre∀(Q2) since {} ⊆ Q2. The analog extreme case holds for suc∃(Q1) and suc∀(Q1) when a state s2 has no predecessors, i.e., pre(s2)={}.

Predecessor and successor sets pre∃(Q2), pre∀(Q2), suc∃(Q1), suc∀(Q1) moreover directly define the semantics of the modal operators in µ-calculus. Thus, they are the basic operations used for model-checking.

Computing pre∃(Φ) symbolically for a formula Φ that denotes a set of states can be done by quantifier elimination of the formula ∃x1′...xn′. R ∧ old2new(φ) where old2new is a function that replaces each variable xi with its corresponding next-state variable xi´. The quantifier elimination is done by the definition of the boolean quantification, i.e., ∃x.φ := [φ]1x ∨ [φ]0x  which means that one can replace the quantification on a variable x by the disjunction of the cofactors on that variable. This has to be done repeatedly, and to make it more efficient, you should better check which is the best variable to start with. 

Similar computations can be done for pre∀(Q2), suc∃(Q1) and suc∀(Q1), and you may also remember that the following hold:

• pre∃(Q2) = S1\pre∀(S2\Q2) 
• pre∀(Q2) = S1\pre∃(S2\Q2) 
• suc∃(Q1) = S2\suc∀(S1\Q1) 
• suc∀(Q1) = S2\suc∃(S1\Q1)

For the universal predecessor, you can directly compute ∀x1′...xn′. R ➞ old2new(φ) where ∀x.φ is defined as the conjunction of the cofactors.

Answer 2

You can find the definition on slide 50 in the transition relation chapter. In my words:

The universal predecessors of Q₂ are all the states that have no successor outside Q₂.

(Formally, a state s₁ is in the universal predecessors of Q₂ iff each state s₂ satisfies an implication that requires that s₂ is in Q₂ if it is a successor of s₁.)

The symbolic formula does nothing else than this. It universally (for all quantifier) quantifies over all primed state variables (vulgo.: right side of the transition relation) and requires for each of them an implication saying: \phi_R → old2new(\phi_Q). The function that I call old2new replaces the unprimed variables by primed variables.

For the existential case, we don't have in implication but a conjuction. Which says that there needs to be a state that is both the successor and in the set we need.

For the universal/existential successor-case, we quantify over the unprimed variables and rename the free variable from primed to unprimed.

Answer 3

To answer the title of the question (i.e. how to compute the universal predecessor):

If you know how to compute the existential one, then based on the duality law, you'd only have to put a negation before the whole thing (so once the existential predecessors are computed just negate the whole thing) and also you have to negate the states for which you are trying to find the universal predecessor.

So if I were to compute the universal predecessor of P, given a transition formula R, it roughly looks like:

Negation( Exists (future variables like Qprime or Pprime) AND (Transition Formula) AND Negation(the state under question) )