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
SN - 2168-2291
VL - 43
SP - 509
EP - 521
JO - IEEE Transactions on Human-Machine Systems
JF - IEEE Transactions on Human-Machine Systems
IS - 6
ER -