Euclidean Model Checking: A Scalable Method for Verifying Quantitative Properties in Probabilistic Systems

In this lecture, I will focus on an alternate method for addressing the problem of large state spaces. For many purposes, it may not be necessary to consider the global state as a cross-product of the states of individual actors. We take our inspiration from statistical physics where macro properties of a system may be related to the properties of individual molecules using probability distributions on the states of the latter. Consider a simple example. Suppose associated with each state is the amount of energy a node consumes when in that state (such an associated value mapping is called the reward function of the state). Now, if we have a frequency count of the nodes in each state, we can estimate the total energy consumed by the system. This suggests a model where the global state is a vector of probability mass functions (pmfs). In the above example, the size of the vector would be 5, one element for each possible state of a node. Each element of the vector represents the probability that any node is in the particular state corresponding to entry.