{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T18:17:54Z","timestamp":1769710674730,"version":"3.49.0"},"reference-count":23,"publisher":"SAGE Publications","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IFS"],"published-print":{"date-parts":[[2023,12,2]]},"abstract":"<jats:p>The self-adaptive multi-agent system requires adaptive adjustments based on the dynamic environment during its runtime. Heterogeneous agent can accomplish different task goals, enhance the efficiency of system operation, but its complex collaboration problem poses new challenges to the study of verification of adaptive policies for heterogeneous multi-agents. This paper proposes a runtime verification method for self-adaptive multi-agent systems using probabilistic timed automata. The method constructs a probabilistic timed automaton model by formally describing the functional characteristics of heterogeneous agents and integrating random factors in the environment to simulate the operation process of the self-adaptive multi-agent system. Regarding the collaboration logic among heterogeneous agents, security constraints are established to ensure the security of state transition processes during system operation. Combining model checking with runtime quantitative verification methods to conduct experiment and applying it in the case of an intelligent unmanned parking system. Experimental results manifest the correctness of the cooperation logic between agents can effectively ensure the stability of the system at runtime. Significant improvement in system uptime and efficiency compared to the initial system without runtime quantitative validation.<\/jats:p>","DOI":"10.3233\/jifs-232397","type":"journal-article","created":{"date-parts":[[2023,9,15]],"date-time":"2023-09-15T11:17:01Z","timestamp":1694776621000},"page":"10305-10322","source":"Crossref","is-referenced-by-count":1,"title":["Runtime verification of self-adaptive multi-agent system using probabilistic timed automata"],"prefix":"10.1177","volume":"45","author":[{"given":"Yongan","family":"Mu","sequence":"first","affiliation":[{"name":"School of Computer Science & Engineering, Wuhan Institute of Technology, Wuhan, China"}]},{"given":"Wei","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Computer Science & Engineering, Wuhan Institute of Technology, Wuhan, China"}]},{"given":"Tao","family":"Lu","sequence":"additional","affiliation":[{"name":"School of Computer Science & Engineering, Wuhan Institute of Technology, Wuhan, China"}]},{"given":"Juan","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science & Engineering, Wuhan Institute of Technology, Wuhan, China"}]},{"given":"Sheng","family":"Gao","sequence":"additional","affiliation":[{"name":"School of Computer Science & Engineering, Wuhan Institute of Technology, Wuhan, China"}]},{"given":"Zihao","family":"Wang","sequence":"additional","affiliation":[{"name":"School of Computer Science & Engineering, Wuhan Institute of Technology, Wuhan, China"}]}],"member":"179","reference":[{"issue":"2","key":"10.3233\/JIFS-232397_ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1516533.1516538","article-title":"Self-adaptive software: Landscape and research challenges","volume":"4","author":"Salehie","year":"2009","journal-title":"ACM Transactions on Autonomous and Adaptive Systems"},{"issue":"1","key":"10.3233\/JIFS-232397_ref3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MC.2003.1160055","article-title":"The vision of autonomic computing","volume":"36","author":"Kephart","year":"2003","journal-title":"Computer"},{"issue":"12","key":"10.3233\/JIFS-232397_ref6","doi-asserted-by":"crossref","first-page":"2812","DOI":"10.1016\/j.jss.2012.04.078","article-title":"Adam: Identifying defects in context-aware adaptation","volume":"85","author":"Chang","year":"2012","journal-title":"Journal of Systems & Software"},{"issue":"6","key":"10.3233\/JIFS-232397_ref11","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/MC.2009.174","article-title":"ASSL: A software engineering approach to autonomic computing","volume":"42","author":"Vassev","year":"2009","journal-title":"Computer"},{"issue":"1","key":"10.3233\/JIFS-232397_ref12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2168260.2168268","article-title":"FORMS: Unifying reference model for formal specification of distributed self-adaptive systems","volume":"7","author":"Weyns","year":"2012","journal-title":"ACM Transactions on Autonomous and Adaptive Systems"},{"issue":"5","key":"10.3233\/JIFS-232397_ref13","first-page":"639","article-title":"Model checking: Software and beyond","volume":"13","author":"Clarke","year":"2008","journal-title":"Journal of Universal Computer Science"},{"issue":"2","key":"10.3233\/JIFS-232397_ref16","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1145\/1186778.1186782","article-title":"A survey of autonomic communications","volume":"1","author":"Dobson","year":"2006","journal-title":"Acm Transactions on Autonomous & Adaptive Systems"},{"issue":"3","key":"10.3233\/JIFS-232397_ref17","doi-asserted-by":"crossref","first-page":"854","DOI":"10.1016\/j.jss.2012.11.055","article-title":"AFChecker: Effective model checking for context-aware adaptive applications","volume":"86","author":"Liu","year":"2013","journal-title":"Journal of Systems & Software"},{"issue":"1","key":"10.3233\/JIFS-232397_ref19","first-page":"23","article-title":"Survey of model-based self-adaptation methods","volume":"29","author":"Zhao","year":"2018","journal-title":"Journal of Software"},{"issue":"2","key":"10.3233\/JIFS-232397_ref25","first-page":"167","article-title":"Runtime-oriented collaborative heterogeneous agent\u2019s capability choosing and compensation","volume":"30","author":"Li","year":"2017","journal-title":"Journal of Yantai University(Natural Science and Engineering Edition)"},{"issue":"7","key":"10.3233\/JIFS-232397_ref26","doi-asserted-by":"crossref","first-page":"1936","DOI":"10.1109\/TAC.2013.2294621","article-title":"On the stabilizability and consensus of positive homogeneous multi-agent dynamical systems","volume":"59","author":"Valcher","year":"2014","journal-title":"IEEE Transactions on Automatic Control"},{"key":"10.3233\/JIFS-232397_ref27","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.automatica.2017.07.011","article-title":"On the consensus of homogeneous multi-agent systems with arbitrarily switching topology","volume":"84","author":"Valcher","year":"2017","journal-title":"Automatica"},{"issue":"9","key":"10.3233\/JIFS-232397_ref28","doi-asserted-by":"crossref","first-page":"2130","DOI":"10.1016\/j.automatica.2011.06.005","article-title":"Stationary consensus of heterogeneous multi-agent systems with bounded communication delays","volume":"47","author":"Liu","year":"2011","journal-title":"Automatica"},{"issue":"3","key":"10.3233\/JIFS-232397_ref30","doi-asserted-by":"crossref","first-page":"1303","DOI":"10.1007\/s11219-019-09486-x","article-title":"Scen@rist: an approach for verifying self-adaptive systems using runtime scenarios","volume":"28","author":"Gadelha","year":"2020","journal-title":"Software Quality Journal"},{"issue":"1","key":"10.3233\/JIFS-232397_ref34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3522585","article-title":"ActivFORMS: A formally founded model-based approach to engineer self-adaptive systems","volume":"32","author":"Weyns","year":"2023","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"C","key":"10.3233\/JIFS-232397_ref36","doi-asserted-by":"crossref","first-page":"107100","DOI":"10.1016\/j.infsof.2022.107100","article-title":"A property specification pattern catalog for real-time system verification with UPPAAL","volume":"154","author":"Vogel","year":"2023","journal-title":"Information and Software Technology"},{"issue":"2","key":"10.3233\/JIFS-232397_ref40","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor Comput Sci"},{"issue":"C","key":"10.3233\/JIFS-232397_ref41","doi-asserted-by":"crossref","first-page":"106004","DOI":"10.1016\/j.asoc.2019.106004","article-title":"Sustainable supplier selection for smart supply chain considering internal and external uncertainty: An integrated rough-fuzzy approach","volume":"87","author":"Chen","year":"2020","journal-title":"Appl Soft Comput"},{"key":"10.3233\/JIFS-232397_ref42","doi-asserted-by":"crossref","first-page":"225272","DOI":"10.1109\/ACCESS.2020.3044929","article-title":"\u015e. \u00c7olak and K. Balikci, Development of a multi-dimensional parametric model with non-pharmacological policies for predicting the COVID-19 pandemic casualties","volume":"8","author":"Tutsoy","year":"2020","journal-title":"IEEE Access"},{"key":"10.3233\/JIFS-232397_ref43","doi-asserted-by":"crossref","first-page":"1265","DOI":"10.1007\/s00158-020-02756-4","article-title":"A methodology for design optimization of powertrain mounting systems involving hybrid interval-random uncertainties","volume":"63","author":"L\u00fc","year":"2021","journal-title":"Structural and Multidisciplinary Optimization"},{"issue":"2","key":"10.3233\/JIFS-232397_ref45","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","article-title":"Model checking for probabilistic timed automata","volume":"43","author":"Norman","year":"2013","journal-title":"Formal Methods in System Design"},{"issue":"5","key":"10.3233\/JIFS-232397_ref47","first-page":"1477","article-title":"Multi-agent adaptive run-time verification based on Markov model","volume":"38","author":"Ye","year":"2021","journal-title":"Application Research of Computers"},{"issue":"4","key":"10.3233\/JIFS-232397_ref48","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","article-title":"Uppaal SMC tutorial","volume":"17","author":"David","year":"2015","journal-title":"International Journal on Software Tools for Technology Transfer"}],"container-title":["Journal of Intelligent &amp; Fuzzy Systems"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JIFS-232397","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T07:21:57Z","timestamp":1769671317000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/JIFS-232397"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,2]]},"references-count":23,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.3233\/jifs-232397","relation":{},"ISSN":["1064-1246","1875-8967"],"issn-type":[{"value":"1064-1246","type":"print"},{"value":"1875-8967","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,2]]}}}