Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Modelling and verification of weighted spiking neural systems
Aman B., Ciobanu G. Theoretical Computer Science623 (C):92-102,2016.Type:Article
Date Reviewed: Jul 13 2016

This paper considers the problem of formal verification of systems described using an abstract computing model called a spiking neural system, which is modeled after how brain cells (neurons) communicate. A spiking neural system is a concurrent set of neurons that communicate with each other using spikes. Each neuron behavior is specified by a finite set of rules that describe how the neuron takes some input spikes and generates some output spikes. The system description specifies how the different neurons in the system are connected, which decides the flow of spikes from one neuron to another. The rules may require some specified number of spikes to be present for their applicability. The application of the rule consumes a fixed number of steps that are specified in the rules. Each neuron is equipped with an initial set of spikes.

The paper proposes the well-known formalism of timed automata for the verification of spiked neural systems. It describes a systematic procedure to convert an arbitrary neural system into a timed automaton: each rule in a neuron is translated into a timed automaton, and the whole system is then converted into a concurrent composition of timed automata. The equivalence between a neural system and the corresponding timed automaton is also established using the notion of bisimulation. The verification of a spiked neural system is then stated as a reachability property in the corresponding timed automata, which can then be verified using the well-known algorithms for timed automata. The paper suggests the use of the tool UPPAAL for the verification of timed automata.

The paper is very readable, especially for those familiar with formal models of computation and formal verification of timed systems. The concepts and methods are well illustrated with examples. However, the scope is narrow and the focus is rather technical.

Reviewer:  S. Ramesh Review #: CR144576 (1610-0753)
Bookmark and Share
  Featured Reviewer  
 
Verification (B.1.4 ... )
 
 
Automata (F.1.1 ... )
 
 
Formal Models (B.1.2 ... )
 
 
Model Checking (D.2.4 ... )
 
 
Neural Nets (C.1.3 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Verification": Date
Formal verification and quantitative metrics of MPSoC data dynamics
Zhang H., Wu J. Formal Aspects of Computing 30(2): 219-237, 2018. Type: Article
Jun 7 2018

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy