Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Probabilistic Model-Checking Framework for Cognitive Assessment and Training

Elisabetta De Maria, Christopher Leturc

TL;DR

The paper develops a probabilistic, formally verifiable framework for cognitive assessment and training using serious games. It models patient behavior with three Probabilistic Deterministic Finite Automaata (PDFA) corresponding to healthy, mild NCD, and Major NCD groups, and orchestrates these with a doxastic meta-automaton that updates practitioner confidence across sessions. The framework employs Probabilistic Temporal Logics (PCTL) and Linear Temporal Logic (LTL) to validate diagnostic properties and training stop conditions, including dynamic adaptation of game difficulty based on observed performance. The work aims to enable diagnosis-support and personalized training in neurodegenerative diseases, with plans to implement a practical tool via PRISM and extend to broader cognitive domains and multiple games.

Abstract

Serious games have proven to be effective tools for screening cognitive impairments and supporting diagnosis in patients with neurodegenerative diseases like Alzheimer's and Parkinson's. They also offer cognitive training benefits. According to the DSM-5 classification, cognitive disorders are categorized as Mild Neurocognitive Disorders (mild NCDs) and Major Neurocognitive Disorders (Major NCDs). In this study, we focus on three patient groups: healthy, mild NCD, and Major NCD. We employ Discrete Time Markov Chains to model the behavior exhibited by each group while interacting with serious games. By applying model-checking techniques, we can identify discrepancies between expected and actual gameplay behavior. The primary contribution of this work is a novel theoretical framework designed to assess how a practitioner's confidence level in diagnosing a patient's Alzheimer's stage evolves with each game session (diagnosis support). Additionally, we propose an experimental protocol where the difficulty of subsequent game sessions is dynamically adjusted based on the patient's observed behavior in previous sessions (training support).

A Probabilistic Model-Checking Framework for Cognitive Assessment and Training

TL;DR

The paper develops a probabilistic, formally verifiable framework for cognitive assessment and training using serious games. It models patient behavior with three Probabilistic Deterministic Finite Automaata (PDFA) corresponding to healthy, mild NCD, and Major NCD groups, and orchestrates these with a doxastic meta-automaton that updates practitioner confidence across sessions. The framework employs Probabilistic Temporal Logics (PCTL) and Linear Temporal Logic (LTL) to validate diagnostic properties and training stop conditions, including dynamic adaptation of game difficulty based on observed performance. The work aims to enable diagnosis-support and personalized training in neurodegenerative diseases, with plans to implement a practical tool via PRISM and extend to broader cognitive domains and multiple games.

Abstract

Serious games have proven to be effective tools for screening cognitive impairments and supporting diagnosis in patients with neurodegenerative diseases like Alzheimer's and Parkinson's. They also offer cognitive training benefits. According to the DSM-5 classification, cognitive disorders are categorized as Mild Neurocognitive Disorders (mild NCDs) and Major Neurocognitive Disorders (Major NCDs). In this study, we focus on three patient groups: healthy, mild NCD, and Major NCD. We employ Discrete Time Markov Chains to model the behavior exhibited by each group while interacting with serious games. By applying model-checking techniques, we can identify discrepancies between expected and actual gameplay behavior. The primary contribution of this work is a novel theoretical framework designed to assess how a practitioner's confidence level in diagnosing a patient's Alzheimer's stage evolves with each game session (diagnosis support). Additionally, we propose an experimental protocol where the difficulty of subsequent game sessions is dynamically adjusted based on the patient's observed behavior in previous sessions (training support).
Paper Structure (24 sections, 6 equations, 6 figures, 1 table)

This paper contains 24 sections, 6 equations, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Case study
  3. Preliminaries
  4. Probabilistic Deterministic Finite Automata
  5. Temporal Logics
  6. The framework: a doxastic meta-automaton
  7. Three PDFA for three classes of patients
  8. An experimental protocol as a meta-automaton
  9. Formal validation
  10. Using PCTL to assess model probabilistic behavior
  11. Reachability of a final state.
  12. Reachability of a precise configuration.
  13. Reachability of a state without violating some constraints.
  14. Reachability of a state without passing from another.
  15. Concatenation of two actions.
  16. ...and 9 more sections

Figures (6)

  • Figure 1: Screenshot of the Match Items game healthinf25
  • Figure 2: Automaton $A_{\mathfrak{h}}$ describing the expected behaviour of healthy people while playing the Match Items serious game healthinf25
  • Figure 3: Automaton of the experimental protocol healthinf25
  • Figure 4: Evolution of $\mathcal{B}_{A_{\mathfrak{h}}}$ in function of $\Delta(w)$healthinf25
  • Figure 5: Evolution of $\mathcal{B}_{A_{\mathfrak{m}}}$ in function of $\Delta(w)$healthinf25
  • ...and 1 more figures

Theorems & Definitions (3)

  • Definition 1
  • Definition 2
  • Definition 3