 Formally, a Basic Finite Modal Probabilistic Model is a tuple \(M=(W,\mathcal{P},V)\), where \(W\) is a finite set of possible worlds or states, \(\mathcal{P}\) is a function associating a distribution \(\mathcal{P}_w\) over \(W\) to each world \(w\in W\), and \(V\) is a ‘valuation function’ assigning atomic propositions from a set \(\Phi\) to each world. The distribution is additively extended from individual worlds to sets of worlds: \(\mathcal{P}_w(S) = \sum_{s\in S}\mathcal{P}_w(s)\). The first two components of a basic modal probabilistic model are effectively the same as a Kripke frame whose relation is decorated with numbers (probability values). Such a structure has different names, such as a directed graph with labelled edges in mathematics, or a probabilistic transition system in computer science. The valuation function, as in a Kripke model, allows us to assign properties to the worlds.