Formal Approaches to Decision-Making under Uncertainty

Course at the Rio 2023 Summer School by Arnd Hartmanns

Software

• For Monday: The Modest Toolset
  (just download and unzip, remember the location)
• For Monday: Visual Studio Code
  (optional, but recommended; otherwise, it is also possible to write models in any text editor and run the Modest Toolset from the command line)
• For Tuesday: GraphViz
  (on Windows, we recommend to install GraphViz in its default location so that the Modest Toolset will most likely find it automatically)
• For Thursday: Python
  (we need version 3.7 or newer)

Do the following steps to configure all the tools to work together:

• For Monday: In Visual Studio Code, install the Modest extension by the Modest Extension Team. Configure the path to the modest executable from the unzipped Modest Toolset folder in the extension's settings.
• New: Patch a bug in the extension by downloading file main.js and placing it into the modestextensionteam.modestextension-0.0.9/media subfolder inside folder %USERPROFILE%\.vscode\extensions on Windows or ~/.vscode/extensions on Linux and macOS, replacing the existing file of the same name.
• For Tuesday: Open a terminal in the Modest folder in the location where you unzipped the Modest Toolset and run the following command:
  modest mosta qcomp://brp -E "N=16,MAX=2" -O brp.dot --dot png brp.png --open-output --delete-output -Y
  If it does not run without errors and (ideally) open some image file, then manually configure the location of the dot executable of GraphViz as described at the end of the Modest installation instructions.
• For Thursday: Set up an environment for programming in Python that you like. For example, in Visual Studio code, install the Python extension pack.

Course Materials

Monday

• Slides: Introduction
• Slides: Discrete-Time Markov Chains
• Slides: Modest Tools for DTMCs (I)
• Model: Córdoba to Rio Cuarto, randomly

Tuesday

• Slides: Modest Tools for DTMCs (II)
• Model: Simulating a die with a coin (flat version)
• Model: Simulating a die with a coin
• Model: Zeroconf protocol
• Slides: Markov Decision Processes
• Slides: Modest Tools for MDPs
• Model: Córdoba to Rio Cuarto with choices (+ scheduler)

Wednesday

• Slides: Algorithms for DTMCs
• Slides: Algorithms for MDPs

Thursday

• Slides: Dealing with Very Large MDPs
• Slides: Anatomy of a Modest Checker
• Code: State Space Explorer (Python demo file)

Miscellaneous

• The Quantitative Verification Benchmark Set contains many examples and case studies using DTMCs, MDPs, and other formalisms to model various kinds of systems. All models are available in the JANI format that the Modest Toolset supports, and many of them were originally written in Modest.
• The PRISM probabilistic model checker supports more complex properties than Modest, has a nice GUI, and extensive documentation. Its input language however is more basic, and it does not have advanced statistical model checking methods or support for continuous-stochastic models like Markov automata.
• The probabilistic model checker Storm is the fastest in most benchmarks, but a little more complex to set up. It can process Modest models via the JANI intermediate format, to which Modest models can be converted with the moconv tool of the Modest Toolset.