Affordable Access

Probabilistic Model Checking for Activity Recognition in Medical Serious Games

Authors
  • L'Yvonnet, Thibaud
  • De Maria, Elisabetta
  • Moisan, Sabine
  • Rigault, Jean-Paul
Publication Date
Jun 03, 2021
Source
HAL
Keywords
Language
English
License
Unknown
External links

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.

Report this publication

Statistics

Seen <100 times