La reconnaissance d'activités humaines joue un rôle important en particulier dans les applications médicales. Cet article propose une approche formelle pour modéliser ces activités en prenant en compte les variations possibles du comportement humain. À partir d'une description de l'activité dans laquelle les probabilité associées aux évènements sont données, nous conceptualisons un modèle formel fondé sur les chaînes de Markov à temps discret. Nous utilisons l'environnement PRISM avec son système de vérification de modèles pour exprimer en logique temporelle et vérifier des propriétés intéressantes concernant l'évolution dynamique des activités. Nous illustrons notre approche avec plusieurs jeux sérieux utilisés par les cliniciens pour évaluer les patients Alzheimer. Nous espérons que cette approche de modélisation apporte de nouvelles indications dans l'interprétation des performances des patients. Cet article se concentre sur la définition des modèles de patients pour trois jeux sérieux ainsi que sur la pertinence d'une telle approche formelle pour vérifier des propriétés sur les comportements de patients ayant un intérêt médical. Il s'agit d'une étape préliminaire obligatoire avant de passer à une étude clinique où de vrais patients joueront à ces jeux. Notre but est de proposer un nouvel outil aux médecins pour évaluer leurs patients.