Probabilistic model checking for human activity recognition in medical serious games

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. Starting from an activity description enriched with event occurrence probabilities, we tra...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2021-06, Vol.206, p.102629, Article 102629
Main Authors: L'Yvonnet, Thibaud, De Maria, Elisabetta, Moisan, Sabine, Rigault, Jean-Paul
Format: Article
Language:English
Subjects:
Activity description
Bio-medicine
Computer Science
Formal Languages and Automata Theory
Life Sciences
Logic in Computer Science
Mathematics
Model checking
Modeling and Simulation
Neurons and Cognition
Probabilistic model
Probability
Psychology and behavior
Serious games
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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. Starting from an activity description enriched with event occurrence probabilities, we translate it into a corresponding formal model based on discrete-time Markov chains (DTMCs). We use the PRISM framework and its model checking facilities to express and check interesting temporal logic properties concerning the dynamic evolution of activities. We illustrate our approach with the models of several serious games used by clinicians to monitor Alzheimer patients. We expect that such a modeling approach could provide new indications for interpreting patient performances. This paper addresses the definition of patient's models for three serious games and the suitability of this approach to check behavioral properties of medical interest. Indeed, this is a mandatory first step before clinical studies with patients playing these games. Our goal is to provide a new tool for doctors to evaluate patients.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2021.102629