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

https://hal.inria.fr/hal-03180187
Contributor : Thibaud l'Yvonnet <>
Submitted on : Wednesday, March 24, 2021 - 6:20:17 PM
Last modification on : Friday, March 26, 2021 - 3:30:09 AM

File

article-reconnaissance.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03180187, version 1

Collections

Citation

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. ⟨hal-03180187⟩

Share

Metrics

Record views

16

Files downloads

148