Description

Model checking allows exact verification of (among others) safety properties on mathematical system formalisations: "the drone will not land on your head." For this, efficient algorithms perform exhaustive exploration on the system states, to compute e.g. the probability of reaching unsafe configurations.

In complex models with probabilistic and nondeterministic choices, such as Markov decision processes (MDPs), value iteration (VI) used to be the algorithm to find a strategy that max- or minimises the probability of reaching an objective. However precise, VI is inefficient in its exploration of the full state space, and no general convergence rule is known to guarantee an epsilon-proximity to the desired max/min probability.

Assignment
Investigate Topological Value Iteration (TVI), a modern variant of VI that circumvents the problem of unnecessary state-value backups by detecting the topological structure of the MDPs' state transition graph. Design, implement, and test TVI in the Modest Toolset: a state-of-the-art verification toolset that supports MDPs and several other modelling formalisms. Compare the performance of TVI vs. VI in challenging models, and aim at possible extensions of TVI to other (orthogonal) VI variants such as Interval Value Iteration.

Research objectives

• Learn about the MDP formalism, the VI algorithm and its limitations, and its extension to TVI.
• Implement TVI for MDP in the Modest Toolset (C#), including ADT choice/development, modularisation, etc.
• Test the implementation on case studies from the literature, such as the bounded exponential backoff procedure.
• Extended objectives:
  • Research variants and extensions of TVI; implement one of them.
  • Extensive experimentation, including new models as of yet unavailable in Modest/JANI.

References

1. The Modest Toolset (Digital version available here)

Additional Resources

1. TVI seminal paper