Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Look-Ahead Simulation Algorithm for DBN Models of Biochemical Pathways Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems

verfasst von : Elisabetta De Maria, Alexandre Muzy, Daniel Gaffé, Annie Ressouche, Franck Grammont

Erschienen in: Hybrid Systems Biology

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Synchronous Balanced Analysis
Nächstes Kapitel Relationship Between the Reprogramming Determinants of Boolean Networks and Their Interaction Graph
Fußnoten
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).
 
Literatur
1.
2.
3.
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 CrossRef
4.
Das, S.: Elements of artificial neural networks [book reviews]. IEEE Trans. Neural Netw. 9(1), 234–235 (1998)CrossRef
5.
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
6.
Franzén, A.: Using satisfiability modulo theories for inductive verification of lustre programs. Electron. Notes Theor. Comput. Sci. 144(1), 19–33 (2006)CrossRefMATH
7.
Gerstner, W., Kistler, W.: Spiking Neuron Models: An Introduction. Cambridge University Press, New York (2002)CrossRefMATH
8.
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
9.
Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic, Dordrecht (1993)CrossRefMATH
10.
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)CrossRef
11.
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)CrossRef
12.
Jeannet, B.: Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Formal Methods Syst. Des. 23(1), 5–37 (2003)CrossRefMATH
13.
Maass, W., Graz, T.U.: Lower bounds for the computational power of networks of spiking neurons. Neural Comput. 8, 1–40 (1995)CrossRef
14.
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)CrossRef
15.
16.
Matsuoka, K.: Mechanisms of frequency and pattern control in the neural rhythm generators. Biol. Cybern. 56(5–6), 345–353 (1987)CrossRef
17.
McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. Bull. Math. Biophys. 5(4), 115–133 (1943)MathSciNetCrossRefMATH
Metadaten
Titel
Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems
verfasst von
Elisabetta De Maria
Alexandre Muzy
Daniel Gaffé
Annie Ressouche
Franck Grammont
Copyright-Jahr
2016
Buch
Hybrid Systems Biology

Print ISBN: 978-3-319-47150-1

Electronic ISBN: 978-3-319-47151-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-47151-8_7

Premium Partner

    Bildnachweise