为独居老人设计个性化日常活动监控框架，用逻辑验证安全行为
A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes
- 基于传感器与访谈数据构建个人化形式模型
- 用线性时序逻辑验证个体行为是否符合安全要求
- 可生成违规原因反推，适合养老科技研究者使用
随着独居老年人口增长，提升其生活质量成为迫切需求。本文提出一种个性化形式验证框架，用于监控居家老人的日常生活活动。该框架整合传感器数据、半结构化访谈、家庭布局及社会观察等上下文信息，为每位参与者构建个性化的形式模型。针对个体需求，将具体要求编码为线性时序逻辑（LTL）性质，并通过模型检测器验证模型是否满足这些性质。当性质被违反时，系统生成反例以揭示违规原因。实验表明，该框架可适用于不同参与者，具有良好的泛化能力，有望提升老年人居家养老的安全性与幸福感。
原文摘要 · Abstract (English)
There is an imperative need to provide quality of life to a growing population of older adults living independently. Personalised solutions that focus on the person and take into consideration their preferences and context are key. In this work, we introduce a framework for representing and reasoning about the Activities of Daily Living of older adults living independently at home. The framework integrates data from sensors and contextual information that aggregates semi-structured interviews, home layouts and sociological observations from the participants. We use these data to create formal models, personalised for each participant according to their preferences and context. We formulate requirements that are specific to each individual as properties encoded in Linear Temporal Logic and use a model checker to verify whether each property is satisfied by the model. When a property is violated, a counterexample is generated giving the cause of the violation. We demonstrate the framework's generalisability by applying it to different participants, highlighting its potential to enhance the safety and well-being of older adults ageing in place.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。