Analysing neurobiological models using communicating automata

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

PDF (Restricted due to publisher copyright policy) - Publisher pdf
Restricted to Repository staff only
Contact us about this Publication Download (676kB)
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
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: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Computational Intelligence Group
Depositing User: Howard Bowman
Date Deposited: 07 Apr 2015 17:17 UTC
Last Modified: 08 May 2018 08:51 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year