Skip to main content

Posts

Showing posts with the label Markov decision processes

Equivalence Checking

There is a compact data structure for words: automata. Finite automata can “store” many words, even infinitely many—in the sense that the language of a finite automaton can be infinite. This powerful feature makes automata ubiquitous in computer science. Lecture notes by Javier Esparza emphasize this view of automata as data structures. The most fundamental algorithmic problems on automata are: operations, such as computing set union or complement of the languages of automata; tests, such as checking their languages for equality. In this post I focus on the latter: equivalence checking. In general, equivalence checking for automata is PSPACE-complete, which is excusable considering how compact and flexible data structures they are. One can check two deterministic finite automata for equivalence in polynomial time, by searching their product. Less known is the fact that one can efficiently check much wider classes of automata for equivalence, including unambiguous auto...

The Price of Memory

In an earlier post I defined the price of memory , $u$, and asked: Is $u < 1$? Worth €100. Determine $u$. Worth another €100, even if $u=1$. I'm happy to announce that there is now a solution: The price of memory, $u$, is 1. I don't want to repeat the precise definition of $u$, but here is a short recap: Suppose you have an acyclic finite MDP and a strategy $\sigma$ that guarantees to visit a red transition with probability 1. This strategy $\sigma$ might use memory, i.e., might base its behaviour in a state on the history of the run, as indicated in yellow: Any such strategy $\sigma$ induces a randomized strategy $\overline\sigma$ that acts like $\sigma$ in average, but is memoryless. In each state, when averaged over all runs, the strategies $\sigma$ and $\overline\sigma$ take the same actions with the same probabilities: One can show that $\sigma$ and $\overline\sigma$ visit red transitions equally often in average; in particular, $\overline\sigma$ visits ...

Tell me the price of memory and I give you €100

Markov Decision Processes (MDPs) are Markov chains plus nondeterminism: some states are random, the others are controlled (nondeterministic). In the pictures, the random states are round, and the controlled states are squares: The random states (except the brown sink state) come with a probability distribution over the successor states. In the controlled states, however, a controller chooses a successor state. What does the controller want to achieve? That depends. In this blog post, the objective is very simple: take a red transition . The only special thing about red transitions is that the controller wants to take them. We consider only MDPs with the following properties: There are finitely many states and transitions. The MDP is acyclic, that is, it has no cycles. There are a unique start state from which any run starts (in the pictures: blue, at the top) and a unique sink state where any run ends (in the pictures: brown, at the bottom). No matter what the controller does, ...

Infinitely many states and no memory

Markov Decision Processes (MDPs) are Markov chains plus nondeterminism: some states are random, the others are controlled (nondeterministic). In the pictures, the random states are round, and the controlled states are squares: The random states come with a distribution over successor states, but in the controlled states a controller chooses a successor state (or a probability distribution over the successor states). For instance, the controller could stay on the leftmost column forever, by always choosing to go one state down. Or the controller could go right at some point; in the random state a successor is picked randomly, either the initial state or the state on the right, according to the blue probabilities. What objective should the controller aim at? In this post, the objective will be the following: visit green states infinitely often, and red states only finitely often . Here is the previous MDP with colours: Since the controller wants to visit (infinitely many) green...