 Formally, a state space is a tuple \({\langle S, \sqsubseteq \rangle}\) where S is a non-empty set of states and \({\sqsubseteq} \subseteq (S \times S)\) is a partial order (i.e., a reflexive, transitive and antisymmetric relation), with \(s_1 \sqsubseteq s_2\) understood as “state \(s_2\) extends state \(s_1\)”. It is assumed that any pair of states has a least upper bound (i.e., a supremum); formally, for any \(s_1, s_2 \in S\) there is \(t_1 \sqcup t_2 \in S\) satisfying