Skip to main content
Kent Academic Repository

Analysing neurobiological models using communicating automata

Su, Li, Gomez, Rodolfo, Bowman, Howard (2014) Analysing neurobiological models using communicating automata. Formal Aspects of Computing, 26 (6). pp. 1169-1204. ISSN 0934-5043. (doi:10.1007/s00165-014-0294-y) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:47880)

PDF (Restricted due to publisher copyright policy) Publisher pdf
Language: English

Restricted to Repository staff only
[thumbnail of Restricted due to publisher copyright policy]
Official URL:


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.

Item Type: Article
DOI/Identification number: 10.1007/s00165-014-0294-y
Uncontrolled keywords: Neuronal networks,Communicating automata,Model checking,Backpropagation, Generalized recirculation algorithm, Plasticity–stability dilemma,Visual attention,Cognitive neuroscience, AI,SPIN,PROMELA,Uppaal
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.87 Neural computers, neural networks
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Howard Bowman
Date Deposited: 07 Apr 2015 17:17 UTC
Last Modified: 17 Aug 2022 10:58 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Gomez, Rodolfo.

Creator's ORCID:
CReDIT Contributor Roles:

Bowman, Howard.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.