Building POMDPs

In Stormvogel, a Partially Observable Markov Decision Process (POMDP) consists of

• states \(S\), actions \(A\), an initial state \(s_0\), a mapping of enabled actions, and a successor distribution \(P(s,a)\), and a labelling function \(L\) as for MDPs,

• a set of observations \(Z\),

• and a deterministic state-observation function \(O\colon S \rightarrow Z\).

The key idea is that the observations encode what information an agent sees. An agent will have to make its decisions not based on the current state, but based on the history of observations it has seen. Note that usually when we refer to MDPs we actually mean fully observable MDPs, which are POMDPs with \(Z = S\) and \(O(s) = s\).

We introduce a simple example to illustrate the difference between MDPs and POMDPs. The idea is that a coin is flipped while the agent is not looking, and then the agent has to guess if it’s heads or tails. We first construct an MDP.

from stormvogel import *

init = ("flip",)


def available_actions(s):
    if "heads" in s or "tails" in s:
        return ["guess_heads", "guess_tails"]
    return [""]


def delta(s, a):
    if s == init:
        return [(0.5, ("heads",)), (0.5, ("tails",))]
    elif a.startswith("guess"):
        if "heads" in s and a == "guess_heads" or "tails" in s and a == "guess_tails":
            return [(1, ("correct", "done"))]
        else:
            return [(1, ("wrong", "done"))]
    else:
        return [(1, s)]


labels = lambda s: list(s)


def rewards(s):
    if "correct" in s:
        return {"R": 100}
    return {"R": 0}


coin_mdp = bird.build_bird(
    delta=delta,
    init=init,
    available_actions=available_actions,
    labels=labels,
    modeltype=ModelType.MDP,
    rewards=rewards,
)
show(coin_mdp)

<stormvogel.visualization.JSVisualization at 0x7fc9241202f0>

Since this MDP is fully observable, the agent can actually see what state the world is in. In other words, the agent knows whether the coin is head or tails. If we ask stormpy to calculate the policy that maximizes the reward, we see that the agent can always ‘guess’ correctly because of this information. The chosen actions are highlighted in red. (More on model checking later.)

result = model_checking(coin_mdp, "Rmax=? [S]")
show(coin_mdp, result=result)

<stormvogel.visualization.JSVisualization at 0x7fc922ac8190>

To model the fact that our agent does not know the state correctly, we will need to use a POMDP! (Note that we re-use a lot of code from before)

def observations(s):
    return 0


coin_pomdp = bird.build_bird(
    delta=delta,
    init=init,
    available_actions=available_actions,
    labels=labels,
    modeltype=ModelType.POMDP,
    rewards=rewards,
    observations=observations,
)

show(coin_pomdp)