Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living

Tommaso Magherini, Alessandro Fantechi, CD Nugent, Enrico Vicario

Research output: Contribution to journalArticle

26 Citations (Scopus)

Abstract

Automated monitoring and the recognition of activities of daily living (ADLs) is a key challenge in ambient-assisted living (AAL) for the assistance of the elderly. Within this context, a formal approach may provide a means to fill the gap between the low-level observations acquired by sensing devices and the high-level concepts that are required for the recognition of human activities. We describe a system named ARA (Automated Recognizer of ADLs) that exploits propositional temporal logic and model checking to support automated real-time recognition of ADLs within a smart environment. The logic is shown to be expressive enough for the specification of realistic patterns of ADLs in terms of basic actions detected by a sensorized environment. The online model checking engine is shown to be capable of processing a stream of detected actions in real time. The effectiveness and viability of the approach are evaluated within the context of a smart kitchen, where different types of ADLs are repeatedly performed.
LanguageEnglish
Pages509-521
JournalIEEE Transactions on Human-Machine Systems
Volume43
Issue number6
DOIs
Publication statusPublished - 2013

Fingerprint

Temporal logic
Model checking
Kitchens
Engines
Specifications
Monitoring
Processing
Assisted living

Cite this

Magherini, Tommaso ; Fantechi, Alessandro ; Nugent, CD ; Vicario, Enrico. / Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living. 2013 ; Vol. 43, No. 6. pp. 509-521.
@article{9645c18f78cf49fca78f60e47a5c4ad3,
title = "Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living",
abstract = "Automated monitoring and the recognition of activities of daily living (ADLs) is a key challenge in ambient-assisted living (AAL) for the assistance of the elderly. Within this context, a formal approach may provide a means to fill the gap between the low-level observations acquired by sensing devices and the high-level concepts that are required for the recognition of human activities. We describe a system named ARA (Automated Recognizer of ADLs) that exploits propositional temporal logic and model checking to support automated real-time recognition of ADLs within a smart environment. The logic is shown to be expressive enough for the specification of realistic patterns of ADLs in terms of basic actions detected by a sensorized environment. The online model checking engine is shown to be capable of processing a stream of detected actions in real time. The effectiveness and viability of the approach are evaluated within the context of a smart kitchen, where different types of ADLs are repeatedly performed.",
author = "Tommaso Magherini and Alessandro Fantechi and CD Nugent and Enrico Vicario",
year = "2013",
doi = "10.1109/TSMC.2013.2283661",
language = "English",
volume = "43",
pages = "509--521",
number = "6",

}

Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living. / Magherini, Tommaso; Fantechi, Alessandro; Nugent, CD; Vicario, Enrico.

Vol. 43, No. 6, 2013, p. 509-521.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living

AU - Magherini, Tommaso

AU - Fantechi, Alessandro

AU - Nugent, CD

AU - Vicario, Enrico

PY - 2013

Y1 - 2013

N2 - Automated monitoring and the recognition of activities of daily living (ADLs) is a key challenge in ambient-assisted living (AAL) for the assistance of the elderly. Within this context, a formal approach may provide a means to fill the gap between the low-level observations acquired by sensing devices and the high-level concepts that are required for the recognition of human activities. We describe a system named ARA (Automated Recognizer of ADLs) that exploits propositional temporal logic and model checking to support automated real-time recognition of ADLs within a smart environment. The logic is shown to be expressive enough for the specification of realistic patterns of ADLs in terms of basic actions detected by a sensorized environment. The online model checking engine is shown to be capable of processing a stream of detected actions in real time. The effectiveness and viability of the approach are evaluated within the context of a smart kitchen, where different types of ADLs are repeatedly performed.

AB - Automated monitoring and the recognition of activities of daily living (ADLs) is a key challenge in ambient-assisted living (AAL) for the assistance of the elderly. Within this context, a formal approach may provide a means to fill the gap between the low-level observations acquired by sensing devices and the high-level concepts that are required for the recognition of human activities. We describe a system named ARA (Automated Recognizer of ADLs) that exploits propositional temporal logic and model checking to support automated real-time recognition of ADLs within a smart environment. The logic is shown to be expressive enough for the specification of realistic patterns of ADLs in terms of basic actions detected by a sensorized environment. The online model checking engine is shown to be capable of processing a stream of detected actions in real time. The effectiveness and viability of the approach are evaluated within the context of a smart kitchen, where different types of ADLs are repeatedly performed.

U2 - 10.1109/TSMC.2013.2283661

DO - 10.1109/TSMC.2013.2283661

M3 - Article

VL - 43

SP - 509

EP - 521

IS - 6

ER -