Temporal Logic Bounded Model-Checking for recognition of activities of daily living

Recognition and monitoring of activities of daily living is a key challenge in the construction of Smart Living environments aimed at supporting independence of elderly or disabled people. In this challenge, there is an opportunity for formal methods to play a crucial role in filling the gap between...

Full description

Saved in:
Bibliographic Details
Main Authors: Magherini, T, Parente, G, Nugent, C D, Donnelly, M P, Vicario, E, Cruciani, F, Paggetti, C
Format: Conference Proceeding
Language:English
Subjects:
Semantics
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Recognition and monitoring of activities of daily living is a key challenge in the construction of Smart Living environments aimed at supporting independence of elderly or disabled people. In this challenge, there is an opportunity for formal methods to play a crucial role in filling the gap between low-level measurements acquired by monitoring systems and high-level concepts that are required for the purposes of decision-support. In this work we propose the application of Temporal Logic and Bounded Model Checking as a way to capture patterns of sequenced activities and recognize them in a stream of observed low-level actions. This approach effectively accommodates for the problems of non-deterministic sequencing and interleaved activities. Results of the implementation and lab-experimentation of the proposed system are presented with reference to the case study within a smart kitchen equipped with stereoscopic camera devices.
ISSN:2168-2194
2168-2208
DOI:10.1109/ITAB.2010.5687608