COMP 524 Model Checking Safety and Dependability Simplified Black Jack. Simplified Black Jack is a game of dice between a player and the bank. It is played with one die in two rounds: in a first round, the player can cast the die several times, in the second round the bank can cast the die several times. The player’s round. Starting with a score of 0, the player can repeatedly • cast her die and • add the number the die shows to her score. After adding the number to her score, she can either stop and hand the die over to the bank, or continue. However, she has lost immediately if her score exceeds 21. The bank’s round. Starting with a score of 0, the bank can (similar to the player in the previous round) repeatedly • cast the die and • add the number the die shows to the bank’s score. The bank has to keep on casting the die until the bank’s score reaches or exceeds the player’s score. The bank has won if the bank’s score at this time does not exceed 21 and lost if the bank’s score at this time exceeds 21. 1. Model the game as a Markov decision process using PRISM or ePMC. (50 marks) 2. Assume that we want to maximise the chance of winning. Write a PRISM property and determine the maximal chance to win. (10 marks) 3. Describe an optimal winning strategy of the player. (10 marks) 4. Assume that we want to minimise the chance of winning. Write a PRISM property and determine the minimal chance to win. (5 marks) Discuss why the chance of winning is like this when the player minimises her chances to win. (5 marks) 5. Change the model such that the bank has to exceed the score of the player to stop. (The player, however, still loses immediately when her score exceeds 21.) Determine the maximial chance for the player to win in this case and discuss the question of whether or not her chance to win is fair (giving a brief justification for your answer). (10 marks) 6. Briefly (≤ 123 words) describe a contemporary research problem associated with Markov chains, Markov games, or Markov decision processes. Cite two recent (from 2016 or younger) articles or conference papers related to the problem you describe. (10 marks) Please hand in (1) executables (the .pm and .pctl files) for the models and properties and (2) an answer that contains the results and explanations. Please form mini groups of two or three students. It is enough if one group member submits, but please include all relevant information on the group – group members (names and student number) – on the first page. good luck!







































学霸联盟