Database of Case Studies Achieved Using CADP

Daily-Living Activity Recognition using Model Checking

Organisation: University Grenoble Alpes
CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG (FRANCE)

Method: MCL

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Smart Homes.

Period: 2017

Size: 1,473,011 events (sensor measurements).

Description: Activity recognition in smart environments is a necessary step for the development of innovative services. In the health-care domain, recognizing activities of daily living (ADL) enables health status monitoring, functional assessments and smart assistance. Despite the broad efforts made in recent years to improve activity recognition, ADL recognition (e.g., cooking, washing dishes, showering) is still not commercially available as is physical activity recognition (e.g., running, cycling).

The first contribution of this study is a rich real-life dataset of daily living activities. This set, named ContextAct@A4H, includes sensor raw data reflecting the context as well as standard daily living annotated activities. Context information can help study how contextual changes affect user behavior and preferences. The dataset was collected using the experimental platform Amiqual4Home, which comprises an apartment equipped with 219 sensors and actuators. For collecting the dataset, a 28 years old woman lived in the apartment during four weeks. The activity monitoring was non-intrusive, using ambient sensors only (no wearable sensors nor cameras). Several context variables were measured: temperature, CO2, noise, humidity, presence and music information, weather information, etc. Appliance and object usage were measured through electric/water consumption sensors, contact sensors and state change sensors (for lamps, curtains and switches).

The second contribution is the automatic detection of activities by analysing the sensor raw data present in the dataset using model checking techniques. The ContextAct@A4H dataset was seen as a log of events, each one containing the occurrence date (including day time), the sensor id, and the sensor value. This log was translated into the SEQ textual format of CADP, accepted as input by the SEQ.OPEN tool. To give simple meanings to complex log events, 125 macro-definitions were written in MCL, and were used subsequently in temporal logic formulas to detect activities in the log. Five different activities were recognized using the EVALUATOR model checker: sleep (start), toilet use (end), cooking (start), taking a shower (end), and washing dishes (start). The average f-measure (a weighted average of the precision and recall) obtained was 0.72, whereas the highest f-measure previously reported in the literature was 0.61.

Conclusions: Using temporal logic allows specifying activities as complex events of object usage, which can be described at different granularities. It also expresses temporal order between events, thus palliating a limitation of ontology based activity recognition. Each activity was described as a temporal logic property that is checked repeatedly on the log of sensor measurements until all occurrences of the activity have been found. One of the main advantages of this approach over other techniques is the ability to recognize start and end of the activity, thus not requiring to segment sensor data.

Publications: [Lago-Lang-Roncancio-et-al-17] P. Lago, F. Lang, C. Roncancio, C. Jiménez-Guarín, R. Mateescu, and N. Bonnefond. The ContextAct@A4H Real-Life Dataset of Daily-Living Activities Activity Recognition using Model Checking. Proceedings of the 10th International and Interdisciplinary Conference on Modeling and Using Context (CONTEXT'2017), Paris, France, LNCS vol. 10257, pages 175-188. Springer Verlag, June 2017.
Available on-line at:
and from our FTP site in PDF or PostScript
Claudia Roncancio
Grenoble INP - ENSIMAG
SIGMA team
Laboratoire d'Informatique de Grenoble
Batiment C - Bureau 223
220, rue de la Chimie
38400 Saint Martin d'Hères
Tel: +33 (0)4 76 63 55 71

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Mon Jan 14 17:12:56 2019.

Back to the CADP case studies page