Abstract. Dementia is the progressive decline in cognitive functions such as thinking, remembering, and reasoning due to damage or disease in the brain. People with advanced dementia have difficulty completing the activities of daily living and need assistance from a caregiver. Cognitive assistive technology that helps guide users through these activities allows this elderly population to complete activities of daily living more independently and can relieve some of the stress of the caregiver. The research project of the COACH system is one of the intelligent systems being developed to assist persons with dementia in such activities, in particular hand-washing.

Based on the research of the COACH system, we model the hand-washing problem as Markov decision processes (MDPs) in PRISM, which is one of the stochastic model checking tools and has been used to analyse systems from a wide range of application domains. This project is a case study of modelling and verification of intelligent systems in PRISM. Various data analysis has been applied to investigate properties of the models.

From the properties checking results, we have identified the factors that play important roles. General rules for choosing policies for different users are summarised. Based on lessons learnt from modelling the hand-washing problem, we present the design of a planning system to help people with dementia during the activity of dressing.