Skip to Main content Skip to Navigation
Conference papers

Probabilistic Model Checking for Activity Recognition in Medical Serious Games

Abstract : Human activity recognition plays an important role especially in medical applications. This paper proposes a formal approach to model such activities, taking into account possible variations in human behavior. This approach is based on discrete-time Markov chains enriched with event occurrence probabilities. We use the PRISM and Storm frameworks and their model checking facilities to express and check interesting temporal logic properties concerning the dynamic evolution of activities. We illustrate our approach on two serious games used by clinicians to monitor Alzheimer patients. This paper focuses on the suitability of such a formal approach to model patients' behavior, to check behavioral properties of medical interest, and on the respective advantages of the PRISM and Storm frameworks. Our goal is to provide a new tool for doctors to evaluate patients.
Complete list of metadata
Contributor : Thibaud l'Yvonnet Connect in order to contact the contributor
Submitted on : Wednesday, March 24, 2021 - 6:20:17 PM
Last modification on : Wednesday, March 16, 2022 - 3:46:32 AM


Files produced by the author(s)




Thibaud l'Yvonnet, Elisabetta de Maria, Sabine Moisan, Jean-Paul Rigault. Probabilistic Model Checking for Activity Recognition in Medical Serious Games. SEH 2021 - 3rd ICSE Workshop on Software Engineering for Healthcare, Jun 2021, Madrid, Spain. ⟨10.1109/SEH52539.2021.00019⟩. ⟨hal-03180187⟩



Record views


Files downloads