Model Checking
Safety and Dependability
Frozen Lake. You want to cross a frozen lake, but beware, it is treacherous!
The lake is a rather abstract lake, formed as a rectangle with 6×4 squares. You start at square (1,1)—the
start, and you want to move to square (6,4)—the goal. In order to do so, you can go up, down, left, or right by de- or incrementing the first or second coordinate, under the condition that the first coordinate has to stay in the value range {1, . . . , 6}, and the second coordinate has to stay in the value range {1, . . . , 4}.
Before you start, 5 holes are randomly inserted in the lake, taking out five squares uniformly at random, excluding the start, the goal, and all positions where there is already a hole.
Claim of Your Friend. Your friend claims that a random walk that merely does not allow moves that would lead into (a hole in) the lake has the same chance of reaching the goal as a well planned path.
1. Model your attempt to cross the lake as a Markov decision processes in IscasMC, ePMC, or PRISM. For this, create a strategic player, who navigates the lake with full knowledge of where the holes are.
(33 marks)
2. Model a random walk as a Markov chain in IscasMC, ePMC, or PRISM. For this replace the strategic player by a random one, who cannot move to any place where a hole has been inserted, but does not plan her walk. (22 marks)
3. Assume you want to maximise your chance of reaching the goal. Write a Probmela (PRISM) property (10 marks) and determine your chance to reach the goal for both models (10 marks). (20 marks)
4. Answer the question raised. (Does a strategically planned walk provide a higher chance to reach the goal than a random walk?) (15 marks)
5. Briefly (≤ 123 words) describe a contemporary research problem associated with Markov chains, Markov games, or Markov decision processes. Cite two recent (from 2017 or younger) articles or conference papers related to the problem you described. (10 marks)
Your model shall be sufficiently detailed such that, in a simulation, you can follow the game. Please hand in:
• a sufficiently commented / explained IscasMC, ePMC, or PRISM model (executable .pm files) for task (1),
• a sufficiently commented / explained IscasMC, ePMC, or PRISM model (executable .pm files) for task (2),
• property files and the results for task (3),
• an answer with an explanation (using whatever it takes) for task (4), and
• a brief description of a research problem, supported by two citations, for task (5).
good luck!