Modelling and analysing neural networks using a hybrid process algebra
Pages 15 - 64
Abstract
Research involving artificial neural networks has tended to be driven towards efficient computation, especially in the domain of pattern recognition, or towards elucidating biological processes in the brain. Models have become more detailed as our understanding of the biology of the brain has increased, incorporating real-time behaviour of individual neurons interacting within complex system structures and dynamics. There are few examples of abstract and fully formal models of biologically plausible neural networks: in the neural networks literature models are often presented as a mixture of mathematical equations and natural language, supported by simulation code and associated experimental results. The informality often hides or obscures important aspects of a particular model, and leaves a large conceptual gap between the model descriptions and the usually low-level programming code used to simulate them.The main contribution of this paper is formally modelling and analysing a biologically plausible neural network model from the literature that exhibits complex neuron-level behaviour and network-level structure. To achieve this a modelling language 'Pann' is developed, based on the process algebras CSP and Hybrid . It is designed to be convenient for mixing the behaviour of discrete events (such as a neuron spike) with mutable continuous and discrete variables (representing chemical properties of a neuron, for instance). Its behaviour is defined using an operational semantics, from which a set of general properties of the language is proved.The groundwork for the biological model is laid by first formalising some well-known concepts from the artificial neural networks domain, such as feedforward behaviour, backpropagation, and recurrent neural networks. The Pann model of a feedforward network, comprising a set of communicating processes representing individual neurons, is proved equivalent to the standard one-line calculation of feedforward behaviour.
References
[1]
W. McCulloch, W. Pitts, A logical calculus of the ideas immanent in nervous activity, Bull. Math. Biophys., 5 (1943) 115-133.
[2]
F. Rosenblatt, The perceptron: a probabilistic model for information storage and organization in the brain, Psychol. Rev., 65 (1958) 386-408.
[3]
E. Izhikevich, J. Gally, G. Edelman, Spike-timing dynamics of neuronal groups, Cereb. Cortex, 14 (2004) 933-944.
[4]
G. Mongillo, O. Barak, M. Tsodyks, Synaptic theory of working memory, Science, 319 (2008) 1543-1546.
[5]
T. Natschläger, W. Maass, Spiking neurons and the induction of finite state machines, Theoret. Comput. Sci., 287 (2002) 251-265.
[6]
W. Maass, H. Markram, On the computational power of circuits of spiking neurons, J. Comput. System Sci., 69 (2004) 593-616.
[7]
M. Ionescu, G. P¿un, T. Yokomori, Spiking neural P systems, Fund. Inform., 71 (2006) 279-308.
[8]
E.M. Izhikevich, Polychronization: computation with spikes, Neural Comput., 18 (2006) 245-282.
[9]
C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985.
[10]
R. Milner, A Calculus of Communicating Systems, Springer-Verlag, Inc., New York, 1982.
[11]
J.A. Bergstra, J.W. Klop, Process algebra for synchronous communication, Inf. Control, 60 (1984) 109-137.
[12]
D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers, Syntax and consistent equation semantics of Hybrid¿, J. Log. Algebr. Program., 68 (2006) 129-210.
[13]
G.D. Plotkin, A structural approach to operational semantics, Computer Science Department, Aarhus University, 1981.
[14]
L. Aceto, W. Fokkink, C. Verhoef, Structural operational semantics, in: Handbook of Process Algebra, Elsevier Science, Amsterdam, 2001, pp. 197-292. http://www.sciencedirect.com/science/article/pii/B9780444828309500217
[15]
C.B. Jones, Understanding programming language concepts via operational semantics, in: Lecture Notes in Computer Science, vol. 4710, Springer, 2007, pp. 177-235.
[16]
R. Colvin, I.J. Hayes, CSP with hierarchical state, in: Lecture Notes in Computer Science, vol. 5423, Springer, 2009, pp. 118-135.
[17]
R.J. Colvin, I.J. Hayes, Structural operational semantics through context-dependent behaviour, J. Log. Algebr. Program., 80 (2011) 392-426.
[18]
J. Fisher, T.A. Henzinger, Executable cell biology, Nat. Biotechnol., 25 (2007) 1239-1249.
[19]
A. Hodgkin, A. Huxley, A quantitative description of membrane current and its application to conduction and excitation in nerve, J. Physiol., 117 (1952) 500-544.
[20]
C. Bishop, Neural Networks for Pattern Recognition, Oxford University Press, 1995.
[21]
E. Fiesler, R. Beale, Handbook of Neural Computation, Oxford University Press, 1996.
[22]
J.M. Spivey, The Z Notation: A Reference Manual, Prentice Hall, 1992.
[23]
D. Rumelhart, G. Hinton, R. Williams, Learning representations by back-propagating errors, Nature, 323 (1986) 533-536.
[24]
R.J. Colvin, I.J. Hayes, A semantics for Behavior Trees using CSP with specification commands, Sci. Comput. Program., 76 (2011) 891-914.
[25]
J.L. Elman, Finding structure in time, Cogn. Sci., 14 (1990) 179-211.
[26]
M. Bodén, A guide to recurrent neural networks and backpropagation, 2002.
[27]
R. Alur, D.L. Dill, A theory of timed automata, Theoret. Comput. Sci., 126 (1994) 183-235.
[28]
J. Bengtsson, W. Yi, Timed automata: semantics, algorithms and tools, in: Lecture Notes in Computer Science, vol. 3098, Springer, 2004, pp. 87-124.
[29]
E. Izhikevich, Simple model of spiking neurons, IEEE Trans. Neural Netw., 14 (2003) 1569-1572.
[30]
E. Izhikevich, Which model to use for cortical spiking neurons?, IEEE Trans. Neural Netw., 15 (2004) 1063-1070.
[31]
S. Song, K. Miller, L. Abbott, Competitive Hebbian learning through spike-timing-dependent synaptic plasticity, Nat. Neurosci., 3 (2000) 919-926.
[32]
H. Markram, Y. Wang, M. Tsodyks, Differential signaling via the same axon of neocortical pyramidal neurons, Proc. Nat. Acad. Sci., 95 (1998) 5323-5328.
[33]
E.M. Izhikevich, Solving the distal reward problem through linkage of STDP and dopamine signaling, Cereb. Cortex, 17 (2007) 2443-2452.
[34]
A. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1998.
[35]
S. Schneider, An operational semantics for timed CSP, Inform. and Comput., 116 (1995) 193-213.
[36]
R. Milner, J. Parrow, D. Walker, Modal logics for mobile processes, Theoret. Comput. Sci., 114 (1993) 149-171.
[37]
G. Plotkin, Call-by-name, call-by-value and the λ-calculus, Theoret. Comput. Sci., 1 (1975) 125-159.
[38]
G.D. Plotkin, A structural approach to operational semantics, J. Log. Algebr. Program., 60-61 (2004) 17-139.
[39]
S. Brookes, A. Roscoe, An improved failures model for communicating processes, in: Lecture Notes in Computer Science, vol. 197, Springer, Berlin/Heidelberg, 1985, pp. 281-305.
[40]
M. Hennessy, R. Milner, On observing nondeterminism and concurrency, in: Lecture Notes in Computer Science, vol. 85, Springer, Berlin/Heidelberg, 1980, pp. 299-309.
[41]
R. Milner, Communication and Concurrency, Prentice Hall, 1989.
[42]
R. van Glabbeek, The linear time - branching time spectrum I, in: Handbook of Process Algebra, North-Holland, 2001, pp. 3-99.
[43]
J. Engelfriet, Determinancy ¿ (observation equivalence = trace equivalence), Theoret. Comput. Sci., 36 (1985) 21-25.
[44]
V. Cortier, S. Delaune, A method for proving observational equivalence, in: Computer Security Foundations Symposium (CSF 2009), IEEE, 2009, pp. 266-276.
[45]
C. Morgan, Programming from Specifications, Prentice Hall, 1994.
[46]
R.J. Back, J. von Wright, Refinement Calculus: A Systematic Introduction, Springer-Verlag, 1998.
[47]
R.D. Simone, Higher-level synchronising devices in Meije-SCCS, Theoret. Comput. Sci., 37 (1985) 245-267.
[48]
M.R. Mousavi, M.A. Reniers, J.F. Groote, SOS formats and meta-theory: 20 years after, Theoret. Comput. Sci., 373 (2007) 238-272.
[49]
B. Bloom, Structural operational semantics for weak bisimulations, Theoret. Comput. Sci., 146 (1995) 25-68.
[50]
I. Ulidowski, I. Phillips, Formats of ordered SOS rules with silent actions, in: Lecture Notes in Computer Science, vol. 1214, Springer, Berlin/Heidelberg, 1997, pp. 297-308.
[51]
R. van Glabbeek, On cool congruence formats for weak bisimulations, in: Lecture Notes in Computer Science, vol. 3722, Springer, Berlin/Heidelberg, 2005, pp. 318-333.
[52]
B. Bloom, S. Istrail, A.R. Meyer, Bisimulation can't be traced, J. ACM, 42 (1995) 232-268.
[53]
J.F. Groote, F. Vaandrager, Structured operational semantics and bisimulation as a congruence, Inform. and Comput., 100 (1992) 202-260.
[54]
X. Nicollin, J. Sifakis, An overview and synthesis on timed process algebras, in: Lecture Notes in Computer Science, vol. 575, Springer, 1992, pp. 376-398.
[55]
P.D. Mosses, Modular structural operational semantics, J. Log. Algebr. Program., 60-61 (2004) 195-228.
[56]
P. Höfner, B. Möller, An algebra of hybrid systems, J. Log. Algebr. Program., 78 (2009) 74-97.
[57]
C.B. Jones, Systematic Software Development Using VDM, Prentice Hall, 1990.
[58]
J.G.G. Borst, J. Soria van Hoeve, The calyx of held synapse: from model synapse to auditory relay, Annu. Rev. Physiol., 74 (2012) 199-224.
[59]
A. Bracciali, M. Brunelli, E. Cataldo, P. Degano, Synapses as stochastic concurrent systems, Theoret. Comput. Sci., 408 (2008) 66-82.
[60]
W. Klimesch, EEG alpha and theta oscillations reflect cognitive and memory performance: a review and analysis, Brain Res. Rev., 29 (1999) 169-195.
[61]
G. Bernot, J.-P. Comet, A. Richard, J. Guespin, Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic, J. Theoret. Biol., 229 (2004) 339-347.
[62]
L. Cardelli, Abstract machines of systems biology, in: Lecture Notes in Computer Science, vol. 3737, Springer, Berlin/Heidelberg, 2005, pp. 145-168.
[63]
L. Calzone, N. Chabrier-Rivier, F. Fages, S. Soliman, Machine learning biochemical networks from temporal logic properties, in: Lecture Notes in Computer Science, vol. 4220, Springer, Berlin/Heidelberg, 2006, pp. 68-94.
[64]
F. Ciocchetta, J. Hillston, Bio-PEPA: a framework for the modelling and analysis of biological systems, Theoret. Comput. Sci., 410 (2009) 3065-3084.
[65]
R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini, An overview on operational semantics in membrane computing, Internat. J. Found. Comput. Sci., 22 (2011) 119-131.
[66]
H. Kugler, A. Larjo, D. Harel, Biocharts: a visual formalism for complex biological systems, J. R. Soc. Interface, 7 (2010) 1015-1024.
[67]
P. Degano, A. Bracciali, Process calculi, systems biology and artificial chemistry, in: Handbook of Natural Computing, 2012, pp. 1863-1896.
[68]
R. Donaldson, M. Calder, Modular modelling of signalling pathways and their cross-talk, Theoret. Comput. Sci., 456 (2012) 30-50.
[69]
R. Rukš¿nas, J. Back, P. Curzon, A. Blandford, Verification-guided modelling of salience and cognitive load, Form. Asp. Comput., 21 (2009) 541-569.
[70]
L. Su, H. Bowman, P. Barnard, B. Wyble, Process algebraic modelling of attentional capture and human electrophysiology in interactive systems, Form. Asp. Comput., 21 (2009) 513-539.
[71]
L. Smith, A framework for neural net specification, IEEE Trans. Softw. Eng., 18 (1992) 601-612.
[72]
I.D. Zaharakis, A.D. Kameas, Modeling spiking neural networks, Theoret. Comput. Sci., 395 (2008) 57-76.
[73]
A. Senyard, E. Kazmierczak, L. Sterling, Software engineering methods for neural networks, in: Tenth Asia-Pacific Software Engineering Conference, 2003, IEEE, 2003, pp. 468-477.
[74]
P.D.d.L. Machado, S.L. Meira, On the use of formal specifications in the design and simulation of artificial neural networks, in: Lecture Notes in Computer Science, vol. 967, Springer, Berlin/Heidelberg, 1995, pp. 63-82.
[75]
G. Dorffner, H. Wiklicky, E. Prem, Formal neural network specification and its implications on standardization, Comput. Stand. Interfaces, 20 (1999) 333-347.
[76]
E. Fiesler, Neural network classification and formalization, Comput. Stand. Interfaces, 16 (1994) 231-239.
[77]
E. Börger, D. Sona, A neural abstract machine, J. Univers. Comput. Sci., 7 (2001) 1006-1023.
[78]
E. Börger, R.F. Stärk, Abstract State Machines. A Method for High-Level System Design and Analysis, Springer, 2003.
[79]
R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini, Compositional semantics of spiking neural P systems, J. Log. Algebr. Program., 79 (2010) 304-316.
[80]
R. Milner, Communicating and Mobile Systems: The π-Calculus, Cambridge University Press, 1999.
[81]
T.A. Henzinger, The theory of hybrid automata, in: NATO ASI Series, vol. 170, Springer, Berlin/Heidelberg, 2000, pp. 265-292.
[82]
T.A. Henzinger, P.-H. Ho, H. Wong-Toi, HyTech: a model checker for hybrid systems, in: Lecture Notes in Computer Science, vol. 1254, Springer, 1997, pp. 460-463.
[83]
G. Frehse, PHAVer: algorithmic verification of hybrid systems past HyTech, in: Lecture Notes in Computer Science, vol. 3414, Springer, Berlin/Heidelberg, 2005, pp. 258-273.
[84]
J. Bergstra, C. Middelburg, Process algebra for hybrid systems, Theoret. Comput. Sci., 335 (2005) 215-280.
[85]
P. Cuijpers, M. Reniers, Hybrid process algebra, J. Log. Algebr. Program., 62 (2005) 191-245.
[86]
M.R. Mousavi, M.A. Reniers, J.F. Groote, Notions of bisimulation and congruence formats for SOS with data, Inform. and Comput., 200 (2005) 107-147.
[87]
D. Gebler, E.-I. Goriac, M.R. Mousavi, Algebraic meta-theory of processes with data, in: Electronic Proceedings in Theoretical Computer Science, vol. 120, Open Publishing Association, 2013, pp. 63-77.
[88]
M. Murphy, K. Reid, D. Hilton, P. Bartlett, Generation of sensory neurons is stimulated by leukemia inhibitory factor, Proc. Nat. Acad. Sci., 88 (1991) 3498-3501.
[89]
H. Jifeng, From CSP to hybrid systems, in: A Classical Mind: Essays in Honour of C.A.R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994, pp. 171-189. http://dl.acm.org/citation.cfm?id=197600.197614
[90]
J. Aimone, J. Wiles, F. Gage, Computational influence of adult neurogenesis on memory encoding, Neuron, 61 (2009) 187.
[91]
D. Buonomano, M. Merzenich, Temporal information transformed into a spatial code by a neural network with realistic properties, Science, 267 (1995) 1028-1030.
[92]
M. Matell, W. Meck, Cortico-striatal circuits and interval timing: coincidence detection of oscillatory processes, Cogn. Brain Res., 21 (2004) 139-170.
[93]
J. Anderson, D. Bothell, M. Byrne, S. Douglass, C. Lebiere, Y. Qin, An integrated theory of the mind, Psychol. Rev., 111 (2004) 1036.
[94]
J. Sanders, G. Smith, Emergence and refinement, Form. Asp. Comput., 24 (2012) 45-65.
[95]
S. Stepney, F. Polack, H. Turner, Engineering emergence, in: 11th IEEE International Conference on Engineering of Complex Computer Systems, 2006, pp. 89-97.
[96]
F. Ciocchetta, A. Duguid, S. Gilmore, M. Guerriero, J. Hillston, The Bio-PEPA tool suite, in: Quantitative Evaluation of Systems (QEST), 2009, pp. 309-310.
[97]
M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, J.F. Quesada, Maude: specification and programming in rewriting logic, Theoret. Comput. Sci., 285 (2002) 187-243.
[98]
P.C. Ölveczky, J. Meseguer, Specification of real-time and hybrid systems in rewriting logic, Theoret. Comput. Sci., 285 (2002) 359-405.
[99]
L. Bortolussi, A. Policriti, Hybrid systems and biology, in: Lecture Notes in Computer Science, vol. 5016, Springer, Berlin/Heidelberg, 2008, pp. 424-448.
[100]
A. David, K.G. Larsen, A. Legay, D.B. Poulsen, Statistical model checking of dynamic networks of stochastic hybrid automata, Electron. Commun. EASST, 66 (2014).
[101]
G. Ferrari, U. Montanari, P. Quaglia, A λ-calculus with explicit substitutions: the late semantics, in: Lecture Notes in Computer Science, vol. 841, Springer, Berlin/Heidelberg, 1994, pp. 342-351.
[102]
MATLAB, Version 7.12.0 (R2011a), The MathWorks Inc., 2011.
[103]
R. Alur, R. Grosu, I. Lee, O. Sokolsky, Compositional refinement for hierarchical hybrid systems, in: Lecture Notes in Computer Science, vol. 2034, Springer, Berlin/Heidelberg, 2001, pp. 33-48.
[104]
I.J. Hayes, C.B. Jones, R.J. Colvin, Laws and semantics for rely-guarantee refinement, Newcastle University, 2014.
[105]
C.B. Jones, I.J. Hayes, R.J. Colvin, Balancing expressiveness in formal approaches to concurrency, Form. Asp. Comput., 27 (2015) 475-497.
[106]
H. Markram, The blue brain project, Nat. Rev., Neurosci., 7 (2006) 153-160.
- Modelling and analysing neural networks using a hybrid process algebra
Recommendations
CN-Nets for Modeling and Analyzing Neural Networks
The concept of colored timed neural Petri nets (CTNPN or Shortly CN-net) which are isomorphic to neural architectures is proposed. The CN-net technique incorporates the basic features of the neural net and the modeling capabilities of both colored and ...
Hybrid high order neural networks
Neural networks (NNs) represent a familiar artificial intelligence approach widely applied in many fields and to a wide range of issues. The back propagation network (BPN) is one of the most well-known NNs, comprising multilayer perceptrons (MLPs) with ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V.
Publisher
Elsevier Science Publishers Ltd.
United Kingdom
Publication History
Published: 11 April 2016
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 03 Jan 2025