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 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.