{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T17:27:10Z","timestamp":1778347630610,"version":"3.51.4"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T00:00:00Z","timestamp":1677715200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2017YFB1401202"],"award-info":[{"award-number":["2017YFB1401202"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Sen. Netw."],"published-print":{"date-parts":[[2023,8,31]]},"abstract":"<jats:p>\n            With the development of the\n            <jats:bold>Internet of Medical Things (IoMT)<\/jats:bold>\n            , indoor\n            <jats:bold>wireless sensor networks (WSNs)<\/jats:bold>\n            have been used to monitor Alzheimer's disease patients daily and guide their behaviors. Alzheimer's disease may seriously impact patients\u2019 memory, and thoughts of \u201cwhat should I do\u201d can unexpectedly form in their mind. This cognitive impairment can affect patients\u2019 independence and well-being. As a basic infrastructure for future healthcare systems, WSN can collect patient behaviors, such as their positions and states, to support safety and health analyses. Therefore, this paper proposes a probabilistic model checking-based method to predict patient behaviors and detect abnormal behaviors related to mild cognitive impairment to help patients rebuild their confidence and perception. First, the layout of the home environment is abstracted as a formal grid, and a\n            <jats:bold>user activity model (UAM)<\/jats:bold>\n            is proposed in the form of\n            <jats:bold>discrete-time Markov chain (DTMC)<\/jats:bold>\n            to describe patients\u2019 activity based on data collected by sensors. Second, because\n            <jats:bold>Alzheimer's patients with mild cognitive impairment (A-MCI)<\/jats:bold>\n            often forget their next daily activities, we classify and describe their daily behaviors as verification requirements in the form of\n            <jats:bold>probabilistic computational tree logic (PCTL)<\/jats:bold>\n            . Then, the UAM is input into a probabilistic model checking tool and compared against the verification property PCTL to calculate the probability values and assess temporal behaviors. As result, the activity with the largest probability is selected for behavior guidance. Third, we demonstrate the process of detecting abnormalities, including activities with abnormal temporal behaviors and activities with normal temporal behaviors but unexpected probabilities that may be repeated more than twice. The key states are extracted from the UAM to specify the verification properties for abnormality detection. Finally, a case study is presented to demonstrate the usability and feasibility of our proposed method.\n          <\/jats:p>","DOI":"10.1145\/3499426","type":"journal-article","created":{"date-parts":[[2022,3,9]],"date-time":"2022-03-09T20:41:46Z","timestamp":1646858506000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Applying Probabilistic Model Checking to the Behavior Guidance and Abnormality Detection for A-MCI Patients under Wireless Sensor Network"],"prefix":"10.1145","volume":"19","author":[{"given":"Honghao","family":"Gao","sequence":"first","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, China"}]},{"given":"Lin","family":"Zhou","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, China"}]},{"given":"Jung Yoon","family":"Kim","sequence":"additional","affiliation":[{"name":"College of Future Industry, Gachon University, Seongnam, South Korea"}]},{"given":"Ying","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science, Zhejiang University, Hangzhou, China"}]},{"given":"Wanqiu","family":"Huang","sequence":"additional","affiliation":[{"name":"School of Computer Science, Zhejiang University, Hangzhou, China"}]}],"member":"320","published-online":{"date-parts":[[2023,3,2]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-4422(19)30290-X"},{"key":"e_1_3_2_3_2","unstructured":"The Lancet"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/JBHI.2017.2777926"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/JBHI.2018.2798062"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11257-020-09266-4"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11042-018-7134-7"},{"key":"e_1_3_2_8_2","first-page":"523","article-title":"Medication adherence monitoring with tracking automation and emergency assistance","year":"2020","unstructured":"Shadab Ali Shaikh, Obaid Kazi, Mohd Adnan Ansari, et al. 2020. Medication adherence monitoring with tracking automation and emergency assistance [C]. International Conference on Mobile Computing and Sustainable Informatics. 523\u2013532.","journal-title":"International Conference on Mobile Computing and Sustainable Informatics"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1159\/000109754"},{"key":"e_1_3_2_10_2","first-page":"1","article-title":"Failure and abnormal behaviour detection in wireless sensor networks","author":"Stegaru Silvia Cristina","year":"2016","unstructured":"Silvia Cristina Stegaru, Emil-Ioan Slu\u015fanschi, Giorgiana Violeta Vl\u0103sceanu, et al. 2016. Failure and abnormal behaviour detection in wireless sensor networks [C]. The 15th RoEduNet Conference: Networking in Education and Research. 1\u20135.","journal-title":"The 15th RoEduNet Conference: Networking in Education and Research"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0921-8890(02)00381-0"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2019.2948204"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jnca.2020.102873"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artmed.2018.06.001"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/MMUL.2010.25"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.2196\/medinform.5587"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11042-017-5452-9"},{"key":"e_1_3_2_18_2","first-page":"723","article-title":"Probabilistic analysis of temporal and sequential aspects of activities of daily living for abnormal behaviour detection","author":"Konios Alexandros","year":"2019","unstructured":"Alexandros Konios, Matias Garcia-Constantino, Stavros-Richard G. Christopoulos, et al. 2019. Probabilistic analysis of temporal and sequential aspects of activities of daily living for abnormal behaviour detection [C]. IEEE SmartWorld. 723\u2013730.","journal-title":"IEEE SmartWorld"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11042-016-3267-8"},{"key":"e_1_3_2_20_2","first-page":"510","article-title":"A sleep pattern analysis and visualization system to support people with early dementia","author":"Nikamalfard Hoda","year":"2011","unstructured":"Hoda Nikamalfard, Huiru Zheng, Haiying Wang, et al. 2011. A sleep pattern analysis and visualization system to support people with early dementia [C]. The 5th International Conference on Pervasive Computing Technologies for Healthcare and Workshops. 510\u2013513.","journal-title":"The 5th International Conference on Pervasive Computing Technologies for Healthcare and Workshops"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2017.12.008"},{"key":"e_1_3_2_22_2","first-page":"143","article-title":"The impact of assistive software application to facilitate people with dementia through participatory research","author":"Asghar Ikram","year":"2020","unstructured":"Ikram Asghar, Shuang Cang, and Hongnian Yu. 2020. The impact of assistive software application to facilitate people with dementia through participatory research [J]. International Journal of Human-Computer Studies (2020), 143, 102471.","journal-title":"International Journal of Human-Computer Studies"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11042-020-08812-x"},{"key":"e_1_3_2_24_2","unstructured":"Soft Computing Volume"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.neucom.2015.09.064"},{"key":"e_1_3_2_26_2","first-page":"89","volume-title":"The 1st ACM SIGMOBILE International Workshop on Systems and Networking Support for Healthcare and Assisted Living Environments","author":"Cuddihy Paul","year":"2007","unstructured":"Paul Cuddihy, Jenny Weisenberg, Catherine Graichen, et al. 2007. Algorithm to automatically detect abnormally long periods of inactivity in a home [C]. The 1st ACM SIGMOBILE International Workshop on Systems and Networking Support for Healthcare and Assisted Living Environments. 89\u201394."},{"key":"e_1_3_2_27_2","first-page":"1","article-title":"Detecting health and behavior change by analyzing smart home sensor data","author":"Sprint Gina","year":"2016","unstructured":"Gina Sprint, Diane Cook, Roschelle Fritz, et al. 2016. Detecting health and behavior change by analyzing smart home sensor data [C]. IEEE International Conference on Smart Computing. 1\u20133.","journal-title":"IEEE International Conference on Smart Computing"},{"key":"e_1_3_2_28_2","first-page":"103","article-title":"Anomaly detection in the elderly daily behavior","author":"Parvin Parvaneh","year":"2018","unstructured":"Parvaneh Parvin, Fabio Patern\u00f2, Stefano Chessa, et al. 2018. Anomaly detection in the elderly daily behavior [C]. The 14th International Conference on Intelligent Environments. 103\u2013106.","journal-title":"The 14th International Conference on Intelligent Environments"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.2174\/1567205015666180427124547"},{"key":"e_1_3_2_30_2","first-page":"309","article-title":"Event-driven framework for detecting unusual patterns in AAL environments","author":"Larcher Lucas","year":"2020","unstructured":"Lucas Larcher, Victor Str\u00f6ele, Mario Dantas, et al. 2020. Event-driven framework for detecting unusual patterns in AAL environments [C]. IEEE 33rd International Symposium on Computer-Based Medical Systems. 309\u2013314.","journal-title":"IEEE 33rd International Symposium on Computer-Based Medical Systems"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3439870"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITB.2006.864480"},{"key":"e_1_3_2_33_2","first-page":"461","article-title":"Probabilistic analysis of abnormal behaviour detection in activities of daily living","author":"Garcia-Constantino Matias","year":"2019","unstructured":"Matias Garcia-Constantino, Alexandros Konios, Idongesit Ekerete, et al. 2019. Probabilistic analysis of abnormal behaviour detection in activities of daily living [C]. IEEE International Conference on Pervasive Computing and Communications Workshops. 461\u2013466.","journal-title":"IEEE International Conference on Pervasive Computing and Communications Workshops"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1080\/09602010343000156"},{"key":"e_1_3_2_35_2","unstructured":"International Joint Conference on Biomedical Engineering Systems and Technologies"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.neucom.2020.05.087"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/TMTT.2019.2939807"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artmed.2019.01.005"},{"key":"e_1_3_2_39_2","first-page":"339","article-title":"A novel stereo positioning method based on optical and SAR sensor","author":"Wu Zhefeng","year":"2014","unstructured":"Zhefeng Wu, Huaping Xu, Huan Zhang, et al. 2014. A novel stereo positioning method based on optical and SAR sensor [C], IEEE Geoscience and Remote Sensing Symposium. 339\u2013342.","journal-title":"IEEE Geoscience and Remote Sensing Symposium"},{"key":"e_1_3_2_40_2","first-page":"327","article-title":"Towards the quantification of human-robot imitation using wearable inertial sensors","author":"Xochicale Miguel P.","year":"2017","unstructured":"Miguel P. Xochicale, Chris Baber, and Mourad Oussalah. 2017. Towards the quantification of human-robot imitation using wearable inertial sensors [C]. In 12th Annual ACM\/IEEE International Conference on Human-Robot Interaction. 327\u2013328.","journal-title":"12th Annual ACM\/IEEE International Conference on Human-Robot Interaction"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3439870"},{"key":"e_1_3_2_42_2","first-page":"1","volume-title":"Wireless Communications and Mobile Computing","author":"Oskouei Jamili","year":"2020","unstructured":"Jamili Oskouei, Dr. Rozita, Mousavi Lou, et al. 2020. IoT-based healthcare support system for Alzheimer's patients [J]. Wireless Communications and Mobile Computing (2020), 1\u201315."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24611-4_5"},{"key":"e_1_3_2_44_2","unstructured":"C. Baier and J. P. Katoen. 2008. Principles of Model Checking [M]. MIT Press 745\u2212907."}],"container-title":["ACM Transactions on Sensor Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3499426","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3499426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:38Z","timestamp":1750188638000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3499426"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,2]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,8,31]]}},"alternative-id":["10.1145\/3499426"],"URL":"https:\/\/doi.org\/10.1145\/3499426","relation":{},"ISSN":["1550-4859","1550-4867"],"issn-type":[{"value":"1550-4859","type":"print"},{"value":"1550-4867","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,2]]},"assertion":[{"value":"2021-07-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-11","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}