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

35 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.
Original languageEnglish
Pages (from-to)509-521
JournalIEEE Transactions on Human-Machine Systems
Volume43
Issue number6
DOIs
Publication statusPublished - 2013

Fingerprint Dive into the research topics of 'Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living'. Together they form a unique fingerprint.

  • Cite this