Abstract
There exists many ways to connect two, three or more neurons together to form different graphs. We call archetypes only the graphs whose properties can be associated with specific classes of biologically relevant structures and behaviors. These archetypes are supposed to be the basis of typical instances of neuronal information processing. To model different representative archetypes and express their temporal properties, we use a synchronous programming language dedicated to reactive systems (Lustre). The properties are then automatically validated thanks to several model checkers supporting data types. The respective results are compared and depend on their underlying abstraction methods.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
With \(w:\,A\rightarrow {\mathbb {Q}}\) for synchronous reactive neurons as discussed later.
- 2.
For the sake of simplicity, we assume that all the synaptic weights are equal to 1; supposing that neuron i has m predecessors, we write \({\varSigma }_{j=1}^{m}x_{j}\) to denote \({\varSigma }_{j\in Pred(i)}x_{j}\); when there is no ambiguity on the neuron index, we do not indicate it.
- 3.
It is not a classical finite state machine because the matrix \(\mathbf {X_{k}}\) considers the current inputs as well as the past inputs received within the integration time window.
- 4.
Observe that all the parameters are multiplied by 10 in order to only deal with integer numbers (and thus to be able to use all the model checkers available to Lustre).
References
Luke webpage. http://www.it.uu.se/edu/course/homepage/pins/vt11/lustre
Nuxmv webpage. https://nuxmv.fbk.eu/
Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 389–448. Springer, Heidelberg (1985). doi:10.1007/3-540-15670-4_19
Das, S.: Elements of artificial neural networks [book reviews]. IEEE Trans. Neural Netw. 9(1), 234–235 (1998)
De Maria, E., Muzy, A., Gaffé, D., Ressouche, A., Grammont, F.: Verification of Temporal Properties of Neuronal Archetypes Using Synchronous Models. Research report 8937, UCA, Inria; UCA, I3S; UCA, LEAT; UCA, LJAD, July 2016. https://hal.inria.fr/hal-01349019
Franzén, A.: Using satisfiability modulo theories for inductive verification of lustre programs. Electron. Notes Theor. Comput. Sci. 144(1), 19–33 (2006)
Gerstner, W., Kistler, W.: Spiking Neuron Models: An Introduction. Cambridge University Press, New York (2002)
Hagen, G., Tinelli, C.: Scaling up the formal verification of lustre programs with SMT-based techniques. In: Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, pp. 1–9, 17–20 November 2008
Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic, Dordrecht (1993)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST ’93). Workshops in Computing, pp. 83–96. Springer, London (1994)
Halbwachs, N., Raymond, P.: Validation of synchronous reactive systems: from formal verification to automatic testing. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol. 1742, p. 1. Springer, Heidelberg (1999)
Jeannet, B.: Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Formal Methods Syst. Des. 23(1), 5–37 (2003)
Maass, W., Graz, T.U.: Lower bounds for the computational power of networks of spiking neurons. Neural Comput. 8, 1–40 (1995)
Maréchal, A., Fouilhé, A., King, T., Monniaux, D., Périn, M.: Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 9583, pp. 166–184. Springer, Heidelberg (2016)
Markram, H.: The blue brain project. Nat. Rev. Neurosci. 7(2), 153–160 (2006)
Matsuoka, K.: Mechanisms of frequency and pattern control in the neural rhythm generators. Biol. Cybern. 56(5–6), 345–353 (1987)
McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. Bull. Math. Biophys. 5(4), 115–133 (1943)
Acknowledgements
The authors would like to thank Gérard Berry for an inspiring talk at the Collège de France (concerning the checking of temporal properties of neuronal structures) as well as for having indicated us the researchers competent at the use of synchronous programming language libraries (in Sophia Antipolis).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
De Maria, E., Muzy, A., Gaffé, D., Ressouche, A., Grammont, F. (2016). Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems. In: Cinquemani, E., Donzé, A. (eds) Hybrid Systems Biology. HSB 2016. Lecture Notes in Computer Science(), vol 9957. Springer, Cham. https://doi.org/10.1007/978-3-319-47151-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-47151-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47150-1
Online ISBN: 978-3-319-47151-8
eBook Packages: Computer ScienceComputer Science (R0)