{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:50:36Z","timestamp":1758970236719,"version":"3.40.4"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2014,11,1]],"date-time":"2014-11-01T00:00:00Z","timestamp":1414800000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Two important issues in computational modelling in cognitive neuroscience are: first, how to formally describe neuronal networks (i.e. biologically plausible models of the central nervous system), and second, how to analyse complex models, in particular, their dynamics and capacity to learn. We make progress towards these goals by presenting a communicating automata perspective on neuronal networks. Specifically, we describe neuronal networks and their biological mechanisms using Data-rich Communicating Automata, which extend classic automata theory with rich data types and communication. We use two case studies to illustrate our approach. In the first case study, we model a number of learning frameworks, which vary in respect of their biological detail, for instance the Backpropagation (BP) and the Generalized Recirculation (GeneRec) learning algorithms. We then used the SPIN model checker to investigate a number of behavioral properties of the neural learning algorithms. SPIN is a well-known model checker for reactive distributed systems, which has been successfully applied to many non-trivial problems. The verification results show that the biologically plausible GeneRec learning is less stable than BP learning. In the second case study, we presented a large scale (cognitive-level) neuronal network, which models an attentional spotlight mechanism in the visual system. A set of properties of this model was verified using Uppaal, a popular real-time model checker. The results show that the asynchronous processing supported by concurrency theory is not only a more biologically plausible way to model neural systems, but also provides a better performance in cognitive modelling of the brain than conventional artificial neural networks that use synchronous updates. Finally, we compared our approach with several other related theories that apply formal methods to cognitive modelling. In addition, the practical implications of the approach are discussed in the context of neuronal network based controllers.<\/jats:p>","DOI":"10.1007\/s00165-014-0294-y","type":"journal-article","created":{"date-parts":[[2014,4,22]],"date-time":"2014-04-22T06:10:11Z","timestamp":1398147011000},"page":"1169-1204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Analysing neurobiological models using communicating automata"],"prefix":"10.1145","volume":"26","author":[{"given":"Li","family":"Su","sequence":"first","affiliation":[{"name":"Department of Psychiatry, University of Cambridge, Level E4, Box 189, Addenbrooke\u2019s Hospital, Hills Road, CB2 0QQ, Cambridge, UK"},{"name":"Department of Psychology, University of Cambridge, Cambridge, UK"}]},{"given":"Rodolfo","family":"Gomez","sequence":"additional","affiliation":[{"name":"Centre for Cognitive Neuroscience and Cognitive Systems, School of Computing, University of Kent, Canterbury, UK"}]},{"given":"Howard","family":"Bowman","sequence":"additional","affiliation":[{"name":"Centre for Cognitive Neuroscience and Cognitive Systems, School of Computing, University of Kent, Canterbury, UK"},{"name":"School of Psychology, University of Birmingham, Birmingham, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.neunet.2008.06.016"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCSI.2002.807515"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Artho C Drusinsky D Goldberg A Havelund K Lowry M Pasareanu C Rosu G Visser W (2003) Experiments with test case generation and runtime analysis. In: Proceedings of the abstract state machines (ASM\u201903). Lecture notes in computer science vol 2589 pp 87\u2013107","DOI":"10.1007\/3-540-36498-6_5"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1162\/089976600300014971"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Barringer H Goldberg A Havelund K Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification model checking and abstract interpretation. Lecture Notes in Computer Science vol 2937 pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"e_1_2_1_2_6_2","unstructured":"Barnard P (1985) Interacting cognitive subsystems: a psycholinguistic approach to short-term memory. In: Ellis A (ed) Progress in the psychology of language vol 2 pp 197\u2013258. Lawrence Erlbaum Associates Ltd. Hove"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Barringer H Goldberg A Havelund K Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification model checking and abstract interpretation. Lecture Notes in Computer Science vol 2937 pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Larsen KG (2004) A tutorial on Uppaal. In: Proceedings of the 4th international school on formal methods for the design of computer communication and software systems (SFM-RT\u201904). Lecture notes in computer science vol 3185 pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bengtsson J Larsen KG Larsson F Pettersson P Yi W (1995) UPPAAL\u2014a tool suite for automatic verification of real-time systems. Hybrid Syst 232\u2013243","DOI":"10.1007\/BFb0020949"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1202043"},{"key":"e_1_2_1_2_11_2","first-page":"25","article-title":"Introduction to the ISO specification language LOTOS","volume":"14910","author":"Bolognesi T","year":"1988","journal-title":"Comput Netw ISDN Syst"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050045"},{"key":"e_1_2_1_2_13_2","unstructured":"Bowman H Derrick J (eds) (2001) Formal methods for distributed processing a survey of object oriented approaches. Cambridge University Press Cambridge"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016000201864"},{"key":"e_1_2_1_2_15_2","unstructured":"Bowman H Gomez RS (2006) Concurrency theory calculi and automata for modelling untimed and timed concurrent systems. Springer New York"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1037\/0033-295X.114.1.38"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.brainres.2007.06.035"},{"key":"e_1_2_1_2_18_2","unstructured":"Clarke EM Grumberg O Peled DA (2000) Model Checking. The MIT Press Cambridge"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1097\/00004647-200110000-00001"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Derrick J Boiten E (2001) Refinement in Z and object-Z: foundations and advanced applications. Springer Berlin","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev.ne.18.030195.001205"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-physiol-021909-135821"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/0010-0277(88)90031-5"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1098\/rstb.2000.0560"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1098\/rstb.2000.0561"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1098\/rstb.2000.0562"},{"key":"e_1_2_1_2_27_2","unstructured":"Garcez AS Broda KB Gabbay DM (2002) Neural-symbolic learning systems foundations and applications. Springer New York"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D Pasareanu C Barringer H (2002) Assumption generation for software component verification. In: Proceedings of the 17th IEEE international conference on automated software engineering pp 3\u201312","DOI":"10.1109\/ASE.2002.1114984"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00344744"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.neunet.2012.09.017"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0893-6080(97)00134-2"},{"key":"e_1_2_1_2_32_2","unstructured":"Havelund K Lowry M Park S Pecheur C Penix J Visser W White JL (2000) Formal analysis of the remote agent before and after flight. In: Proceedings of 5th NASA Langley formal methods workshop pp 13\u201315"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1113\/jphysiol.1952.sp004764"},{"key":"e_1_2_1_2_35_2","unstructured":"Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley Boston"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Kiczales G Lamping J Mendhekar A Maeda C Lopes CV Loingtier JM Irwin J (1997) Aspect-oriented programming. In: Lecture notes in computer science vol 1241. Springer-Verlag New York","DOI":"10.1007\/BFb0053381"},{"key":"e_1_2_1_2_37_2","unstructured":"Kolen JF Pollack JB (1991) Back propagation is sensitive to initial conditions. In Lippmann RP Moody JE Touretzky DS (eds) Advances in neural information processing systems vol 3 pp 860\u2013867"},{"key":"e_1_2_1_2_38_2","unstructured":"Liljenstr\u00f6m H (1994) Cognition neurodynamics and computer models. Connectionism in a broad perspective. Ellis Horwood Chichester"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Springer New York","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_1_2_40_2","first-page":"154","article-title":"Verification and validation and artificial intelligence","volume":"65","author":"Menzies T","year":"2005","journal-title":"Adv Comput"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Moller F Tofts CMN (1990) A temporal calculus of communicating systems. In: CONCUR\u201990 pp 401\u2013415","DOI":"10.1007\/BFb0039073"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Napolitano MR Molinaro G Innocenti M Seanor B Martinelli D (1999) A complete hardware package for a fault-tolerant flight control system using on-line learning neural networks. In: Proceedings of the American Control Conference pp 2615\u20132619","DOI":"10.1109\/ACC.1999.786541"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1037\/0096-3445.134.3.291"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0042-6989(97)00169-7"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1162\/neco.1996.8.5.895"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"O\u2019Reilly RC Munakata Y (2000) Computational explorations in cognitive neuroscience: understanding the mind by simulating the brain. MIT Press Cambridge","DOI":"10.7551\/mitpress\/2014.001.0001"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium foundations of computer science FOCS 1977 pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Rodrigues P Costa JF Siegelmann HT (2001) Verifying properties of neural networks. Artificial and natural neural networks. In: Lecture notes in computer science vol 2084 pp 158\u2013165 Springer New York","DOI":"10.1007\/3-540-45720-8_19"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Rolls ET Deco G (2002) Computational neuroscience of vision. Oxford University Press Oxford","DOI":"10.1093\/acprof:oso\/9780198524885.001.0001"},{"key":"e_1_2_1_2_50_2","unstructured":"Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall London"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0102-7"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.148478"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1162\/neco.1996.8.6.1301"},{"key":"e_1_2_1_2_54_2","unstructured":"Su L Bowman H Barnard PJ (2007) Attentional capture by meaning a multi-level modelling study. In: Proceedings of 29th annual meeting of the Congitive Science Society Nashville pp 1521\u20131526"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0094-3"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Su L Bowman H Barnard P (2011) Glancing and then looking: on the role of body affect and meaning in cognitive control. Front Psychol 2:348 doi:10.3389\/fpsyg.2011.00348","DOI":"10.3389\/fpsyg.2011.00348"},{"issue":"2","key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","first-page":"129","DOI":"10.3758\/BF03337828","article-title":"Configural association theory: the role of the hippocampal formation in learning, memory, and amnesia","volume":"17","author":"Sutherland RJ","year":"1989","journal-title":"Psychobiology"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1080\/14640749108400971"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0294-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0294-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0294-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:10:48Z","timestamp":1746195048000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0294-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11]]},"references-count":58,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,11]]}},"alternative-id":["10.1007\/s00165-014-0294-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0294-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2014,11]]}}}