{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:23Z","timestamp":1781193743543,"version":"3.54.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_9","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:34:04Z","timestamp":1781192044000},"page":"192-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Analysis of\u00a0Stochastic Cognitive Models: A Translation Framework from\u00a0Soar to\u00a0PRISM"],"prefix":"10.1007","author":[{"given":"Parth","family":"Ganeriwala","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Candice","family":"Chambers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James I.","family":"Lathrop","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Siddhartha","family":"Bhattacharyya","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Junaid","family":"Babar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen B.","family":"Gilbert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Isaac","family":"Amundson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael C.","family":"Dorneich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammed Abdul Hafeez","family":"Khan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Amundson, I., et al.: Modeling and formal analysis of high-assurance mixed-reality systems. In: 2025 AIAA DATC\/IEEE 44th Digital Avionics Systems Conference (DASC), pp. 1\u201310 (2025). https:\/\/doi.org\/10.1109\/DASC66011.2025.11257175","DOI":"10.1109\/DASC66011.2025.11257175"},{"issue":"4","key":"9_CR2","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.1037\/0033-295X.111.4.1036","volume":"111","author":"JR Anderson","year":"2004","unstructured":"Anderson, J.R., et al.: An integrated theory of the mind. Psychol. Rev. 111(4), 1036 (2004)","journal-title":"Psychol. Rev."},{"key":"9_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. Formal Methods Des. Real-Time Syst. 200\u2013236 (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Bhattacharyya, S., Neogi, N., Eskridge, T., Carvalho, M., Stafford, M.: Formal assurance for cooperative intelligent agents. In: NASA Formal Methods Symposium LNCS, vol. 10811 (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_2","DOI":"10.1007\/978-3-319-77935-5_2"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bhattacharyya, S., Davis, J., Gupta, A., Narayan, N., Matessa, M.: Assuring increasingly autonomous systems in human-machine teams: an urban air mobility case study. In: Formal Methods for Autonomous Systems, vol.\u00a0348, pp. 150\u2013166 (2021). https:\/\/doi.org\/10.4204\/eptcs.348.11","DOI":"10.4204\/eptcs.348.11"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Bolton, M.L., Bass, E.J.: Enhanced operator function model (EOFM): a task analytic modeling formalism for including human behavior in the verification of complex systems. In: The Handbook of Formal Methods in Human-computer Interaction, pp. 343\u2013377. Springer (2017)","DOI":"10.1007\/978-3-319-51838-1_13"},{"issue":"3","key":"9_CR8","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1109\/TSMCA.2012.2210406","volume":"43","author":"ML Bolton","year":"2013","unstructured":"Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: Using formal verification to evaluate human-automation interaction: a review. IEEE Trans. Syst. Man Cybern. Syst. 43(3), 488\u2013503 (2013)","journal-title":"IEEE Trans. Syst. Man Cybern. Syst."},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The NUXMV symbolic model checker. In: CAV, pp. 334\u2013342 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"9_CR10","doi-asserted-by":"crossref","first-page":"143252","DOI":"10.1109\/ACCESS.2024.3421660","volume":"12","author":"J Duan","year":"2024","unstructured":"Duan, J., et al.: Study of cybersickness in augmented reality railway inspections applications. IEEE Access 12, 143252\u2013143262 (2024)","journal-title":"IEEE Access"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Ganeriwala, P., et al.: Design and validation of learning aware HMI for learning-enabled increasingly autonomous systems. In: 2025 IEEE International Systems Conference (SysCon), pp.\u00a01\u20138. IEEE (2025). https:\/\/doi.org\/10.1109\/SysCon64521.2025.11014784","DOI":"10.1109\/SysCon64521.2025.11014784"},{"key":"9_CR12","unstructured":"Ganeriwala, P., Matsumuro, M., Ritter, F.E., Bhattacharyya, S.: Enabling formal verification in a common model of cognition (2025). https:\/\/sbp-brims.org\/2025\/papers\/working-papers\/2025_SBP-BRiMS_paper_18.pdf, sBP-BRiMS 2025 Working Paper"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Ganeriwala, P., et al.: Systems engineering with architecture modeling, formal verification, and human interactions for learning-enabled autonomous agent. Syst. Eng. (2025)","DOI":"10.1002\/sys.21816"},{"key":"9_CR14","unstructured":"Grumberg, O., Clarke, E., Peled, D.: Model checking. In: International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer: Berlin\/Heidelberg, Germany (1999)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Guntupalli, L., Li, F.Y.: DTMC modeling for performance evaluation of DW-MAC in wireless sensor networks. In: 2016 IEEE Wireless Communications and Networking Conference, pp.\u00a01\u20136. IEEE (2016)","DOI":"10.1109\/WCNC.2016.7564772"},{"issue":"1","key":"9_CR16","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s10462-018-9646-y","volume":"53","author":"I Kotseruba","year":"2020","unstructured":"Kotseruba, I., Tsotsos, J.K.: 40 years of cognitive architectures: core cognitive abilities and practical applications. Artif. Intell. Rev. 53(1), 17\u201394 (2020)","journal-title":"Artif. Intell. Rev."},{"issue":"4","key":"9_CR17","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Prism: probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Perform. Eval. Rev. 36(4), 40\u201345 (2009)","journal-title":"ACM SIGMETRICS Perform. Eval. Rev."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: verification of probabilistic real-time systems. In: International Conference on Computer Aided Verification, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"9_CR19","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1146\/annurev-control-042820-010947","volume":"5","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Annu. Rev. Control Robot. Auton. Syst. 5(1), 385\u2013410 (2022)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Laird, J.: The SOAR Cognitive Architecture. MIT Press (2012). https:\/\/doi.org\/10.7551\/mitpress\/7688.001.0001","DOI":"10.7551\/mitpress\/7688.001.0001"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Laird, J., Rosenbloom, P., Newell, A.: Chunking in soar: the anatomy of a general learning mechanism. Mach. Learn. 1, 11\u201346 (1986). https:\/\/doi.org\/10.1007\/BF00116249","DOI":"10.1007\/BF00116249"},{"issue":"4","key":"9_CR22","first-page":"13","volume":"38","author":"JE Laird","year":"2017","unstructured":"Laird, J.E., Lebiere, C., Rosenbloom, P.S.: A standard model of the mind: toward a common computational framework across artificial intelligence, cognitive science, neuroscience, and robotics. AI Mag. 38(4), 13\u201326 (2017)","journal-title":"AI Mag."},{"key":"9_CR23","unstructured":"Langenfeld, V., Westphal, B., Podelski, A.: On formal verification of ACT-R architectures and models. In: Proceedings of the Annual Meeting of the Cognitive Science Society, vol. 41 (2019)"},{"issue":"2","key":"9_CR24","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/j.cogsys.2006.07.004","volume":"10","author":"P Langley","year":"2009","unstructured":"Langley, P., Laird, J.E., Rogers, S.: Cognitive architectures: research issues and challenges. Cogn. Syst. Res. 10(2), 141\u2013160 (2009)","journal-title":"Cogn. Syst. Res."},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Narayan, N., et al.: Assuring learning-enabled increasingly autonomous systems*. In: 2023 IEEE International Systems Conference (SysCon), pp.\u00a01\u20137 (2023). https:\/\/doi.org\/10.1109\/SysCon53073.2023.10131227","DOI":"10.1109\/SysCon53073.2023.10131227"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Nason, S., Laird, J.: Soar-RL: integrating reinforcement learning with Soar. Cogn. Syst. Res. 6, 51\u201359 (2005). https:\/\/doi.org\/10.1016\/j.cogsys.2004.09.006","DOI":"10.1016\/j.cogsys.2004.09.006"},{"issue":"9","key":"9_CR27","doi-asserted-by":"publisher","first-page":"6028","DOI":"10.1109\/TITS.2021.3076399","volume":"22","author":"N Neogi","year":"2021","unstructured":"Neogi, N., Bhattacharyya, S., Griessler, D., Kiran, H., Carvalho, M.: Assuring intelligent systems: contingency management for UAS. IEEE Trans. Intell. Transp. Syst. 22(9), 6028\u20136038 (2021). https:\/\/doi.org\/10.1109\/TITS.2021.3076399","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511810633"},{"key":"9_CR29","doi-asserted-by":"crossref","first-page":"788","DOI":"10.1016\/j.procs.2018.11.029","volume":"145","author":"OJ Romero","year":"2018","unstructured":"Romero, O.J.: CogArch-ADL: toward a formal description of a reference architecture for the common model of cognition. Procedia Comput. Sci. 145, 788\u2013796 (2018)","journal-title":"Procedia Comput. Sci."},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Sun, R.: Anatomy of the mind: exploring psychological mechanisms and processes with the Clarion cognitive architecture. Oxford University Press (2016)","DOI":"10.1093\/acprof:oso\/9780199794553.001.0001"},{"issue":"2","key":"9_CR31","doi-asserted-by":"crossref","first-page":"83","DOI":"10.55676\/asi.v4i2.81","volume":"4","author":"J Tomaszewska","year":"2023","unstructured":"Tomaszewska, J.: Application of Markov chains, MTBF and machine learning in air transport reliability. Aviat. Secur. Issues 4(2), 83\u2013106 (2023)","journal-title":"Aviat. Secur. Issues"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Wang, T.E., Amundson, I., Babar, J., Wu, P.: Formal analysis of vulnerabilities in mixed-reality systems. In: IEEE International Conference on Systems, Man, and Cybernetics (2025)","DOI":"10.1109\/SMC58881.2025.11343623"},{"issue":"4","key":"9_CR33","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1111\/1467-8721.00184","volume":"11","author":"CD Wickens","year":"2002","unstructured":"Wickens, C.D.: Situation awareness and workload in aviation. Curr. Dir. Psychol. Sci. 11(4), 128\u2013133 (2002)","journal-title":"Curr. Dir. Psychol. Sci."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:34:10Z","timestamp":1781192050000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}