Hello,

the definition of universal predecessors in set theory is pre∀(Q) := {s1 ∈ S | suc(s1) ⊆ Q}, i.e. all states of S that have all their successors (if any) in Q. If a state has no successors it is also contained in pre∀(Q).

The definition of pre∀(Q) in propositional logic is the following, with φ being the formula that symbolically represents Q and R being the formula of the symbolic transition relation:

pre∀(φ) :⇔ ∀x1′ . . . xn′. R → old2new(φ)

(old2new(): substitutes state variables xi with next state variables xi').

In the set representation, also all states that have no successors are contained. But since those states have no outgoing transitions, they are not contained in R → old2new(φ) and therefore also not represented by pre∀(φ). Is that correct or have I done a mistake?

Best regards,

choehne