Remark Logic for control [efr-002P]

Let an MDP (or partially observable MDP) be given, and consider a statement like "given policy \pi , the expected reward is \geq r", or "the probability that the total reward is less than r is \leq \epsilon ", and so on. In one sense, these are statements about policies---but, fixing a policy, they become statements about the states of the MDP (meaning: if the problem is initialized in state s_0, and we use policy \pi , ...). In particular, they are statements about the behaviour of the state of the MDP, and so should be expressible using the modal logic.

In particular, given a system TS \to A, if we have a good way of controlling the composite system TS \to A \to B---that is, a modal formula providing that certain behavior on the interface will lead to a high reward---then we can translate this into a statement that certain behavior on the interface A (namely, the same behaviour translated back) will lead to a high reward in the original system. Moreover, we're not restricted to statements about expected reward, but can encode all sorts of statements about the behavior, like a bound on the probability that some region will be crossed.