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.

翻译：随着独居老年人口不断增长，提升其生活质量已成为迫切需求。以人为中心、兼顾个人偏好与情境的个性化解决方案至关重要。本研究提出一种用于表示与推理独居老年人日常生活活动的框架。该框架整合了传感器数据与情境信息，后者汇总了参与者的半结构化访谈、住宅布局及社会学观察数据。基于这些数据，我们构建了根据参与者偏好与情境定制的个性化形式化模型。我们将针对每个个体的特定需求编码为线性时序逻辑属性，并利用模型检验器验证模型是否满足各属性。当属性被违反时，系统会生成反例以揭示违规原因。通过将该框架应用于不同参与者，我们验证了其普适性，彰显了其在提升居家养老老年人安全与福祉方面的潜力。