{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T07:31:37Z","timestamp":1761291097572,"version":"3.37.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,6,14]],"date-time":"2020-06-14T00:00:00Z","timestamp":1592092800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,14]],"date-time":"2020-06-14T00:00:00Z","timestamp":1592092800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004543","name":"China Scholarship Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004543","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1007\/s10270-020-00807-4","type":"journal-article","created":{"date-parts":[[2020,6,14]],"date-time":"2020-06-14T03:24:37Z","timestamp":1592105077000},"page":"429-445","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An improved approach on the model checking for an agent-based simulation system"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9711-2118","authenticated-orcid":false,"given":"Yinling","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haiqing","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Cheutet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,14]]},"reference":[{"key":"807_CR1","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.cosrev.2017.03.001","volume":"24","author":"S Abar","year":"2017","unstructured":"Abar, S., Theodoropoulos, G.K., Lemarinier, P., O\u2019Hare, G.M.P.: Agent based modelling and simulation tools: a review of the state-of-art software. Comput. Sci. Rev. 24, 13\u201333 (2017)","journal-title":"Comput. Sci. Rev."},{"key":"807_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.simpat.2014.11.003","volume":"51","author":"F Al-Saqqar","year":"2015","unstructured":"Al-Saqqar, F., Bentahar, J., Sultan, K., Wan, W., Asl, E.K.: Model checking temporal knowledge and commitments in multi-agent systems using reduction. Simul. Model. Pract. Theory 51, 45\u201368 (2015)","journal-title":"Simul. Model. Pract. Theory"},{"issue":"2","key":"807_CR3","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1016\/j.eswa.2012.07.069","volume":"40","author":"J Bentahar","year":"2013","unstructured":"Bentahar, J., Yahyaoui, H., Kova, M., Maamar, Z.: Symbolic model checking composite Web services using operational and control behaviors. Expert Syst. Appl. 40(2), 508\u2013522 (2013)","journal-title":"Expert Syst. Appl."},{"key":"807_CR4","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 1\u201318. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_1"},{"issue":"2","key":"807_CR5","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"RH Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. Auton. Agents Multi-agent Syst. 12(2), 239\u2013256 (2006)","journal-title":"Auton. Agents Multi-agent Syst."},{"key":"807_CR6","unstructured":"Cavada, R., Cimatti, A., Keighren, G., Olivetti, E., Pistor, M., Roveri, M.: NuSMV 2.5 Tutorial. (2019). Accessed 1 Mar 2019. http:\/\/nusmv.fbk.eu\/NuSMV\/tutorial\/v25\/tutorial.pdf"},{"key":"807_CR7","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri. M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: International Conference on Computer Aided Verification, pp. 359\u2013364. Springer (2002). http:\/\/nusmv.fbk.eu\/","DOI":"10.1007\/3-540-45657-0_29"},{"key":"807_CR8","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/j.jss.2017.12.042","volume":"138","author":"M El Menshawy","year":"2018","unstructured":"El Menshawy, M., Bentahar, J., El Kholy, W., Laarej, A.: Model checking real-time conditional commitment logic using transformation. J. Syst. Softw. 138, 189\u2013205 (2018)","journal-title":"J. Syst. Softw."},{"key":"807_CR9","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R Fagin","year":"2004","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning about knowledge. MIT Press, Cambridge (2004)"},{"issue":"1","key":"807_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s10458-004-3140-4","volume":"10","author":"M Fisher","year":"2005","unstructured":"Fisher, M.: Temporal development methods for agent-based. Auton. Agents Multi-agent Syst. 10(1), 41\u201366 (2005)","journal-title":"Auton. Agents Multi-agent Syst."},{"key":"807_CR11","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/j.simpat.2012.12.007","volume":"32","author":"J Joo","year":"2013","unstructured":"Joo, J., Kim, N., Wysk, R.A., Rothrock, L., Son, Y.-J., Yeong-gwang, O., Lee, S.: Agent-based simulation of affordance-based human behaviors in emergency evacuation. Simul. Model. Pract. Theory 32, 99\u2013115 (2013)","journal-title":"Simul. Model. Pract. Theory"},{"key":"807_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2016.07.006","volume":"124","author":"B Keshanchi","year":"2017","unstructured":"Keshanchi, B., Souri, A., Navimipour, N.J.: An improved genetic algorithm for task scheduling in the cloud environments using the priority queues: formal verification, simulation, and statistical testing. J. Syst. Softw. 124, 1\u201321 (2017)","journal-title":"J. Syst. Softw."},{"key":"807_CR13","doi-asserted-by":"crossref","unstructured":"Liu, Y., Wang, T., Zhang, H., Cheutet, V.: Information systems simulation for performance evaluation-application in aircraft maintenance. In: IFIP International Conference on Product Lifecycle Management, pp. 789\u2013799. Springer (2018)","DOI":"10.1007\/978-3-030-01614-2_72"},{"key":"807_CR14","doi-asserted-by":"publisher","first-page":"106041","DOI":"10.1016\/j.cie.2019.106041","volume":"137","author":"Y Liu","year":"2019","unstructured":"Liu, Y., Wang, T., Zhang, H., Cheutet, V., Shen, G.: The design and simulation of an autonomous system for aircraft maintenance scheduling. Comput. Ind. Eng. 137, 106041 (2019)","journal-title":"Comput. Ind. Eng."},{"key":"807_CR15","doi-asserted-by":"crossref","unstructured":"Liu, Y., Ngu, A.H., Zeng, L.Z.: QoS computation and policing in dynamic web service selection. In: Proceedings of the 13th International World Wide Web Conference on Alternate Track Papers and Posters, pp. 66\u201373. ACM (2004)","DOI":"10.1145\/1013367.1013379"},{"key":"807_CR16","doi-asserted-by":"crossref","unstructured":"Maamar, Z., Sheng, Q.Z., Yahyaoui, H., Bentahar, J., Boukadi, K.: A new approach to model web services\u2019 behaviors based on synchronization. In: International Conference on Advanced Information Networking and Applications Workshops, 2009. WAINA\u201909, pp. 43\u201349. IEEE (2009)","DOI":"10.1109\/WAINA.2009.65"},{"issue":"2","key":"807_CR17","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1057\/jos.2016.7","volume":"10","author":"CM Macal","year":"2016","unstructured":"Macal, C.M.: Everything you need to know about agent-based modelling and simulation. J. Simul. 10(2), 144\u2013156 (2016)","journal-title":"J. Simul."},{"issue":"3","key":"807_CR18","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1057\/jos.2010.3","volume":"4","author":"CM Macal","year":"2010","unstructured":"Macal, C.M., North, M.J.: Tutorial on agent-based modelling and simulation. J. Simul. 4(3), 151\u2013162 (2010)","journal-title":"J. Simul."},{"issue":"4","key":"807_CR19","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/s10458-013-9232-2","volume":"28","author":"A Meski","year":"2014","unstructured":"Meski, A., Penczek, W., Szreter, M., Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A.: BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Auton. Agents Multi-agent Syst. 28(4), 558\u2013604 (2014)","journal-title":"Auton. Agents Multi-agent Syst."},{"key":"807_CR20","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.compind.2014.12.007","volume":"68","author":"NJ Navimipour","year":"2015","unstructured":"Navimipour, N.J., Navin, A.H., Rahmani, A.M., Hosseinzadeh, M.: Behavioral modeling and automated verification of a Cloud-based framework to share the knowledge and skills of human resources. Comput. Ind. 68, 65\u201377 (2015)","journal-title":"Comput. Ind."},{"key":"807_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"807_CR22","volume-title":"Model checking multi-agent systems","author":"F Raimondi","year":"2006","unstructured":"Raimondi, F.: Model checking multi-agent systems. University of London, London (2006). PhD diss"},{"key":"807_CR23","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.simpat.2018.04.002","volume":"85","author":"A Serrano-Hernandez","year":"2018","unstructured":"Serrano-Hernandez, A., Faulin, J., Hirsch, P., Fikar, C.: Agent-based simulation for horizontal cooperation in logistics and transportation: from the individual to the grand coalition. Simul. Model. Pract. Theory 85, 47\u201359 (2018)","journal-title":"Simul. Model. Pract. Theory"},{"issue":"3","key":"807_CR24","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1109\/MIC.2010.78","volume":"14","author":"QZ Sheng","year":"2010","unstructured":"Sheng, Q.Z., Maamar, Z., Yahyaoui, H., Bentahar, J., Boukadi, K.: Separating operational and control behaviors: a new approach to Web services modeling. IEEE Internet Comput. 14(3), 68\u201376 (2010)","journal-title":"IEEE Internet Comput."},{"key":"807_CR25","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/j.simpat.2018.05.009","volume":"86","author":"W Song","year":"2018","unstructured":"Song, W., Xi, H., Kang, D., Zhang, J.: An agent-based simulation system for multi-project scheduling under uncertainty. Simul. Model. Pract. Theory 86, 187\u2013203 (2018)","journal-title":"Simul. Model. Pract. Theory"},{"issue":"8","key":"807_CR26","doi-asserted-by":"publisher","first-page":"3831","DOI":"10.1016\/j.eswa.2013.11.042","volume":"41","author":"A Souri","year":"2014","unstructured":"Souri, A., Navimipour, N.J.: Behavioral modeling and formal verification of a resource discovery approach in Grid computing. Expert Syst. Appl. 41(8), 3831\u20133849 (2014)","journal-title":"Expert Syst. Appl."},{"key":"807_CR27","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Alternating automata and program verification. In: Computer Science Today, pp. 471\u2013485. Springer (1995)","DOI":"10.1007\/BFb0015261"},{"issue":"2","key":"807_CR28","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1504\/IJWGS.2010.033787","volume":"6","author":"H Yahyaoui","year":"2010","unstructured":"Yahyaoui, H., Maamar, Z., Boukadi, K.: A framework to coordinate web services in composition scenarios. Int. J. Web Grid Serv. 6(2), 95\u2013123 (2010)","journal-title":"Int. J. Web Grid Serv."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00807-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00807-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00807-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,13]],"date-time":"2021-06-13T23:13:23Z","timestamp":1623626003000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00807-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,14]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["807"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00807-4","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2020,6,14]]},"assertion":[{"value":"20 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 January 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 May 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}