Probabilistic Modeling and Verification of an Adaptive VR Serious Game for Patients with Cognitive Impairment

Serious games proved to be an effective tool for screening cognitive deficits and aiding in the diagnosis of neurodegenerative diseases like Alzheimer's and Parkinson's. Additionally, they are recognized for their benefits in cognitive training. In this work, we introduce a new serious game targeting inhibitory control, a cognitive function often impaired in Alzheimer's and Parkinson's patients. The specificity of this game is proposing an inhibitory control task in immersive virtual reality with adaptive difficulty adjustment based on the patient's performance. After modeling the game as a Discrete Time Markov Chain, we use the probabilistic Model Checker Prism to verify the model with respect to some crucial dynamic properties and to retrieve the probabilities associated with some classes of paths describing the patient's gameplay. This formal approach aims to support the medical staff in spotting the differences between expected and observed behavior.