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.