<figure><img src="image_1.png" /></figure>

HAL
open science

# Probabilistic Modeling of Spiking Neural Networks with Contract-Based Verification

Zhen Yao, Elisabetta de Maria, Robert de Simone

► To cite this version:

Zhen Yao, Elisabetta de Maria, Robert de Simone. Probabilistic Modeling of Spiking Neural Networks with Contract-Based Verification. UCNC 2025 - 22th International Conference on Unconventional Computation and Natural Computation, Enrico Formenti, Sep 2025, Nice, France. hal-05416855

HAL Id: hal-05416855

https://inria.hal.science/hal-05416855v1

Submitted on 15 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Probabilistic Modeling of Spiking Neural
Networks with Contract-Based Verification

Zhen Yao¹[0009-0007-4848-7689], Elisabetta De Maria¹[0000-0001-7116-9629], and Robert De Simone²[0000-0002-3123-7591]

¹ Université Côte d'Azur, I3S, CNRS, France

zhen.yao@etu.univ-cotedazur.fr, edemaria@i3s.unice.fr

² Centre Inria d'Université Côte d'Azur, France

robert.de_simone@inria.fr

**Abstract.** Spiking Neural Networks (SNN) are models for "realistic" neuronal computation, which makes them somehow different in scope from "ordinary" deep-learning models widely used in AI platforms nowadays. SNNs focus on timed latency (and possibly probability) of neuronal reactive activation/response, more than numerical computation of filters. So, an SNN model must provide modeling constructs for elementary neural bundles and then for synaptic connections to assemble them into compound data flow network patterns. These elements are to be parametric patterns, with latency and probability values instantiated on particular instances (while supposedly constant "at runtime"). Designers could also use different values to represent "tired" neurons, or ones impaired by external drugs, for instance. One important challenge in such modeling is to study how compound models could meet global reaction requirements (in stochastic timing challenges), provided similar provisions on individual neural bundles. A temporal language of logic to express such assume/guarantee contracts is thus needed. This may lead to formal verification on medium-sized models and testing observations on large ones. In the current article, we make preliminary progress at providing a simple model framework to express both elementary SNN neural bundles and their connecting constructs, which translates readily into both a model-checker and a simulator (both already existing and robust) to conduct experiments.

**Keywords:** Spiking Neural Networks · Bio-inspired Computing · Probabilistic Model Checking · Neuronal Circuits · Formal Methods.

# 1 Introduction

Spiking Neural Networks constitute the third generation of neural network models, marrying computational efficiency with biological plausibility. Unlike traditional rate-based Artificial Neural Networks (ANNs), SNNs employ event-driven spikes—discrete voltage pulses—to encode and transmit information, focusing on the timed latency and probabilistic nature of neuronal activation. This mechanism greatly reduces energy consumption by activating
neurons only when spikes occur, and naturally captures temporal dynamics, making SNNs well-suited for tasks involving time-varying inputs such as signal processing, motor control, and event-based vision [15].

Early demonstrations have shown that SNNs can match ANNs on both classical benchmarks (e.g., MNIST, N-MNIST, N-Caltech101) [10,14] and more challenging datasets like ImageNet and CIFAR-10 [17], while preserving their energy-saving advantages. Beyond performance, the bio-inspired nature of SNNs renders them invaluable for neuroscientific inquiry, offering a computational window into the dynamics of real neural circuits. Central to SNN performance is the choice of neuron model, which must balance biological realism against computational tractability. Leaky Integrate-and-Fire (LI&F) neurons afford efficiency but neglect some dynamics; biophysically detailed Hodgkin-Huxley models capture a wealth of ionic processes at the cost of prohibitive computational load [9]. Recent advances—in particular, Generalized Leaky Integrate-and-Fire (GLIF) [18] and Noisy LI&F [16] models—have introduced stochastic thresholds and membrane-potential noise to better mimic cortical variability. However, existing variants still fall short of emulating absolute and relative refractory behaviors observed in biological neurons.

In this paper, we introduce the **Refractory-evolve Probabilistic Leaky Integrate-and-Fire (RP-LI&F)** neuron model based on previous Boolean Probabilistic Spiking Neural Network [4]. RP-LI&F embeds discrete-time refractory dynamics and probabilistic spike generation into the LI&F framework, yielding a compact yet biologically grounded unit. We support RP-LI&F with a domain-specific format, Spiking Neural Networks Representation File (SNN-RF), that automatically produces discrete-time Markov chain models for formal verification in PRISM and high-performance simulations in Nengo [1].

SNN models require parametric constructs for elementary neural bundles and synaptic connections, enabling the assembly of complex data-flow network patterns. These constructs must support the instantiation of latency and probability parameters, which remain constant during runtime but can vary to simulate conditions such as neuronal fatigue or pharmacological effects. A key challenge is ensuring that compound SNN models meet global reaction requirements under stochastic timing constraints, given similar provisions for individual neural bundles. This necessitates a temporal logic language to express assume/guarantee contracts, facilitating formal verification for medium-sized models and testing through simulation for larger ones.

This preliminary work aims to develop a brain-like neural network by archetypes [2], which are specific neuronal micro-circuits, that can be combined in the future to form complicated, brain-inspired systems, distinct from second-generation networks focused solely on data processing efficiency. The remainder of this paper is structured as follows. Section 2 introduces our RP-LI&F neuron model. Section 3 describes the PRISM model checker with the logic PCTL and the Nengo simulator. Section 4 presents how we automatically generate a network model in both Nengo and PRISM via SNN-RF. Section 5 details case studies demonstrating RP-LI&F in contralateral inhibition and
convergent excitatory circuit, two fundamental archetypes [2]. Finally, Section 6 concludes and outlines directions for future work. The code can be found at https://github.com/zxy1553/RP-LIF.git.

## 2 Refractory-Evolve Probabilistic LI&F Model

Real neurons maintain a resting voltage that slowly drifts back after synaptic inputs, fire when they reach a threshold, exhibit random channel-driven fluctuations, and pause briefly after each spike before regaining full excitability. In our RP-LI&F abstraction, the leak factor $r = \exp(-\Delta t/\tau_m)$ models the passive return to rest, the threshold $\tau$ marks the voltage for spike initiation, the membrane potential $p(t)$ sums incoming spikes with exponential decay, discrete probability levels $\{p_i\}$ capture channel noise that makes firing stochastic, the absolute-refractory countdown ARP enforces a short window of zero spiking, and the relative-refractory countdown RRP with scaling factor $\alpha$ represents the gradual restoration of firing probability after an action potential.

We define the **Refractory-evolve Probabilistic Leaky Integrate-and-Fire** (RP-LI&F) neuron as a tuple $v = (\tau, r, p, y, s, aref, rref)$, where:

- $\tau \in \mathbb{N}$: reference firing threshold

- $r \in [0, 1] \cap \mathbb{Q}$: leak factor, governing exponential decay of potential.

- $p: \mathbb{N} \to \mathbb{Q}_0^+$: membrane potential at discrete time $t$, with

$$p(t) = \begin{cases} \sum_{i=1}^{m} w_i x_i(t), & \text{if } y(t-1) = 1, \\ \sum_{i=1}^{m} w_i x_i(t) + r p(t-1), & \text{otherwise,} \end{cases} \quad (1)$$

where $p(0) = 0$, $m$ is the number of inputs, $w_i$ the synaptic weight, and $x_i(t) \in \{0, 1\}$ the incoming spike.

- $y: \mathbb{N} \to \{0, 1\}$: output spike function, $y(t) = 1$ iff a spike is emitted at $t$.

- $s \in \{0, 1, 2\}$: state flag, taking values 0 for Normal period, 1 for Absolute refractory period, and 2 for Relative refractory period.

- aref $\in \{0, \dots, \text{ARP}\}$: absolute-refractory countdown,

- rref $\in \{0, \dots, \text{RRP}\}$: relative-refractory countdown.
## 2.1 Spike-Probability Law

Let $\Delta(t) = p(t) - \tau$. Let us discretize $\Delta$ into $2k+1$ intervals $\{-l_k, \dots, 0, \dots, l_k\}$. We define a base firing probability as follows:

$$ P_{\text{base}}(y(t) = 1) = \begin{cases} 1, & \Delta(t) \ge l_k, \\ p_{2k}, & l_{k-1} \le \Delta(t) < l_k, \\ \vdots \\ p_{k+1}, & 0 \le \Delta(t) < l_1, \\ p_k, & -l_1 \le \Delta(t) < 0, \\ \vdots \\ p_1, & -l_k \le \Delta(t) < -l_{k-1}, \\ 0, & \Delta(t) < -l_k. \end{cases} $$

Here, $\{p_i\}$ are predefined probabilities over $\Delta/\tau$. Then the actual spike probability is

$$ P(y(t) = 1) = \begin{cases} 0, & s = 1, \\ \alpha P_{\text{base}}(y(t) = 1), & s = 2, \\ P_{\text{base}}(y(t) = 1), & s = 0, \end{cases} $$

with $\alpha \in [0, 1]$ shrinking relative-refractory firing.

## 2.2 Refractory Dynamics

*Absolute Refractory Period (s = 1)* For this step after a spike, $y(t) = 0$ always, $p(t) \equiv 0$, and $\text{aref} \to \text{aref} - 1$ each step. When $\text{aref} = 0$, transition to $s = 2$.

*Relative Refractory Period (s = 2)* For this step, the neuron may fire at a reduced rate $\alpha P_{\text{base}}$. $\text{rref}$ decrements until zero; if a spike occurs, reset $\text{aref}$ and re-enter $s = 1$, else when $\text{rref} = 0$, return to $s = 0$.

Figure 1 illustrates the three-state finite-state machine governing transitions among Normal, Absolute, and Relative refractory periods based on spike events and counters.

# 3 SNN Toolchain Overview

This section introduces the PRISM model checker for formal verification and Nengo for simulation. PRISM allows one to model systems with probability aspects and to verify dynamic properties. Nengo leverages the Neural Engineering Framework (NEF) to build and simulate mechanistic neuronal circuits. Together, they offer a comprehensive approach to designing, validating, and analyzing SNNs.
<figure><img src="image_3.png" /><figcaption>Fig. 1: RP-LI&F neuron state transitions.</figcaption></figure>

## 3.1 PRISM

PRISM [13] is a powerful framework designed for probabilistic modeling and verification, enabling the analysis of diverse probabilistic systems such as discrete and continuous-time Markov chains (DTMCs and CTMCs), Markov Decision Processes (MDPs). In addition to modeling, PRISM supports the formal specification of system behavior using probabilistic temporal logics, including PCTL [8] (Probabilistic Computation Tree Logic).

**Syntax and modeling** We model our SNN as a DTMC by representing each neuron or population as a PRISM module with local variables capturing membrane potential and spike events. Guarded commands of the form:

$$[action] guard \rightarrow prob_1 : update_1 + \dots + prob_n : update_n;$$

encode probabilistic spiking and rest behaviors. Synchronization labels *action* ensure coordinated updates across neurons at each time step. Reward structures are added to track metrics such as total spikes or energy consumption, enabling queries of the form: $R\{"y"\} =? [C^{\leq 100}]$ to compute expected spike counts within a time bound.

**PCTL and Model Checking** PRISM employs PCTL to define the DTMCs with probabilistic and temporal constraints. PCTL extends CTL with a probabilistic path quantifier (e.g. $P_{\geq p}[F \phi]$ and time bounds).
All quantifiers except **X** support time-bounded variants (e.g., $F \leq^t \phi$). The
**P** =? [prop] form computes the exact probability of a property.

In our workflow, we automatically generate the PRISM model from a
high-level description of the network topology: connectivity matrices, synaptic
weights, and firing thresholds are parsed to instantiate modules and commands.
We then specify PCTL queries for key properties and invoke PRISM's model
checker to compute exact probabilities.

## 3.2 Nengo

Nengo is a neural modeling and simulation platform based on the NEF, which uses populations of spiking neurons to represent and transform vectors mechanically [5]. Users define networks via a Python API, specifying Ensembles (populations), Connections (transformations), and Probes (recordings).

We construct each SNN circuit in Nengo to align with the PRISM model: ensembles correspond to PRISM modules, and synaptic filters model transition probabilities. Simulation run on CPU or Liohi hardware generates spike trains and state trajectories over time. Probe data is exported to show how neurons in the neural network work. Both the DTMC abstraction and the NEF implementation are important to ensure our neural network works as we suppose.

# 4 Automated SNN generation and modeling

In this section, we present a structured approach to modeling SNNs, encompassed in a dedicated representation file format (SNN-RF), itself compliant for translation to both PRISM and Nengo analysis frameworks. By defining both individual neuron archetypes and combining network properties in YAML-based representation files, we enable the automatic generation of models for both simulation and formal verification. This method simplifies the configuration of complex neural architectures, such as those based on our custom Refractory-evolve Probabilistic Leaky Integrate-and-Fire (RP-LI&F) neurons, while ensuring consistency across different modeling tools.

We begin by outlining the structure and purpose of these representation files, followed by detailing how they are used to generate PRISM and Nengo models. Finally, we provide insights into the implementation details within each tool, highlighting the custom neuron models and their behaviors.

## 4.1 Representation Files

The SNN-RF format essentially provides a parametric description of the elementary neuron archetypes (in the present case RP-LI&F), and the synaptic connections to combine and associate them in larger structures. Distinct neurons can be instantiated by fixing local values for the parameters (timing and probability thresholds of reactive spikes). The simple YAML form of SNN-RF is designed to allow simple and correct translation into PRISM and Nengo, and also
to promote easily readable configuration of parameters and network topologies through lists and dictionaries.

Importantly, the single source ensures that the resulting PRISM and Nengo descriptions have identical behaviors and therefore allows cross-validation between simulation and model-checking results. Currently, correctness requirements are expressed only directly using PCTL probabilistic temporal logic in PRISM, but in the future, our SNN-RF format should also provide simple parametric requirement patterns to be translated both in PCTL for PRISM and as runtime observers for Nengo.

Below is a snippet from our network representation file:

```python
network:
    name: "STRING"  # type of neural network
    simulate:
        steps: INTEGER
    inputs:
        - id: INTEGER
          value: INTEGER
        ...
    n_neurons:
        - id: INTEGER
          # More properties for neurons in the network
        ...
    edges:
        - from:
            type: STRING
            id: INTEGER
        to:
            type: STRING
            id: INTEGER
        weight: INTEGER
        ...
```

<caption>Listing 1.1: Spiking Neuron Network Representation File</caption>

## 4.2 Neuron for PRISM

Our SNN comprises multiple modules, collectively forming a complete DTMC model. Typically, the model includes an input layer, a synapse layer, and an output layer. Each neuron receives a single input signal, and all inputs are grouped into the Input module. Neurons are assigned distinct weights for their binary inputs (restricted to 0 or 1). Neuron modules are named by combining their type with a unique identifier (e.g., Neuron1), enabling the expansion of our model into multi-layer architectures. Neurons across different layers are interconnected through synapses implemented as transfer modules. The Input, neuron, and transfer modules serve as the foundational building blocks of our network, enabling the generation of various archetypes. The core neuron behavior is encapsulated in a Neuron module:

```python
module Neuron1
    aref : [0..ARP] init 0; // absolute refractory
    rref : [0..RRP] init 0; // relative refractory

s: [0..2] init 0; // state
```
```python
y: [0..1] init 0; // spike
p: [-500..500] init P_restore; // membrane potential

[to] s = 0 & y = 0 & p < threshold1 ->
    1.0: (y' = 0) & (p' = newPotential);

[to] ...
[to] s = 0 & y = 0 &
    p >= threshold5 & p < threshold6 ->
    0.5: (y' = 0) & (p' = newPotential) +
    0.5: (y' = 1);

[to] ...
[to] s = 0 & y = 0 & p > threshold10 ->
    1.0: (y' = 1);

endmodule
```

The neuron spikes ($y = 1$) when its potential exceeds a threshold, resetting to a basic value and entering an absolute refractory period ($s = 1$). We implement the update in Equation 1 by first taking the weighted sum plus the leak term, rounding it down to an integer, and then clipping the result to lie between MAX and MIN, where MAX and MIN denote the upper and lower bounds of the discretized membrane potential: $newPotential = \max(\min(\sum_{i=1}^{m} w_i x_i + r \cdot p], MAX), MIN)$, which ensures our discrete membrane potential remains within the specified bounds. Moreover, a rewards structure counts spikes:

```
rewards "spike1_count"
y1 = 1 : 1;
endrewards
```

enabling precise analysis of network activity.

## 4.3 Neuron for Nengo

Nengo's standard neurons lack probabilistic spiking and refractory periods, so we introduce ProbNeuron, based on our RP-L&F model, to address these limitations. Using Nengo's API, we build networks with single-neuron ensembles (encoder=1) and a step delay to align with PRISM models. We probe spike activity, membrane potential, and state, synchronizing the time step $dt$ with PRISM's Markov chain for consistent, high-precision verification and simulation.

The behavior of our RP-L&IF neuron is encapsulated in the ProbNeuron class:

```python
class ProbNeuron(nengo.neurons.NeuronType):
    def __init__(self, P_rth=10, P_restore=0,
                 r=0.7, ARP=2, RRP=5, alpha=0.08, dt=0.001):
        super().__init__()
        self.P_rth = P_rth  # threshold
        self.ARP = ARP      # absolute refractory
        self.RRP = RRP      # relative refractory
        self.alpha = alpha  # shrinking factor
```
```python
self.dt = dt          # time step

def step(self, dt, J, output, **state):
    s = state["s"]   # state
    p = state["p"]  # membrane potential
    y = state["y"]  # spike
    if s == 0:
        # normal state
        p = np.floor(J + self.r * p)
        prob = self.get_spike Prob(p, is_rrp=False)
        y = 1 if np.random rand() < prob else 0
    # ... (handle refractory period)
    output[...] = y
```

# 5 Case Study

We validate our framework with one RP-LI&F neuron, two archetypes: contralateral inhibition and convergent excitatory circuit. These demonstrate our approach for probabilistic verification and simulation, using SNN-RF to generate consistent DTMCs and Nengo Ensembles with shared *dt* time steps, ensuring precise cross-domain validation (Figures 3, 5). All experiments were performed on a machine with an Intel(R) Core(TM) i5-8300H CPU @ 2.30 GHz, 16 GB RAM, running ARCH LINUX (kernel version 6.14.6.arch1-1).

## 5.1 RP-L&IF Neuron

Before we go into those two cases, first, we present the verification and simulation of only one RP-LI&F neuron to understand better how our neuron works. Here, we checked the correct implementation of the RP-LI&F neuron. The input of this neuron is a constant one (see Figure 2a).

**PCTL properties and results** We validated the fundamental characteristics of the RP-LI&F neuron, specifically its transition rules and spiking probabilities, which are essential for all subsequent developments.

$P_1: P_{>=1}[G((y_1 = 1) \rightarrow (X(s = 1)))]$ verified that whenever a spike occurs, the very next state is the absolute refractory period, in which the neuron does not emit.

$P_2: P_{>=1}[G((s = 1 \land aref=0) \rightarrow (X(s = 2 \land rref=RRP)))]$ asserts that when aref reaches 0 in state 1, the next state is 2 with rref reset to its maximum.

$P_3: P_{=?}[(p > threshold5) \land (p \le threshold6)] \rightarrow (X(y = 1))$ checks the correctness of one of our probabilistic transitions. All the others can also be proved to be 1 in probability.

Table 1 shows the outcomes and execution time of Properties $P_1$ to $P_3$.

**Nengo Simulation** The Nengo simulation results (see Figure 2b) illustrate a single neuron's spiking behavior and state transitions.
<figure><img src="image_4.png" /><figcaption>Fig. 2: RP-LI&F Neuron and Simulation (the X-axis represents time, and the Y-axis, from top to bottom, represents spike, membrane potential, and states)</figcaption></figure>

<table><caption>Table 1: Verification Results of RP-LI&F Neuron</caption><thead><tr><th>Properties</th><th>Specifications</th><th>Outcomes</th><th>Time</th></tr></thead><tbody><tr><td>P<sub>1</sub></td><td>P<sub>&gt;=1</sub>[G((y<sub>1</sub> = 1) &rarr; (X (s = 1)))]</td><td>True</td><td>45 ms</td></tr><tr><td>P<sub>2</sub></td><td>P<sub>&gt;=1</sub>[G((s = 1 &amp; aref = 0) &rarr; (X (s = 2 &amp; rref = RRS)))]</td><td>True</td><td>19 ms</td></tr><tr><td>P<sub>3</sub></td><td>P<sub>=?</sub>[(p &gt; threshold<sub>5</sub>) &amp; (p &lt;= threshold<sub>6</sub>)] &rarr; (X (y<sub>1</sub> = 1))]</td><td>0.5</td><td>9 ms</td></tr></tbody></table>

## 5.2 Contralateral Inhibition

Contralateral Inhibition models neural populations that mutually suppress activity, a mechanism critical to sensory processing. They provide an elementary computation that can be used for decision-making (not only simple forms of behavioral choices but also more complex choices) [12]. As another example, active and passive fear responses are mediated by distinct and mutually inhibitory central amygdala neurons [6]. Here we provide a network that consists of one input always being 1, and two RP-L&IF neurons which inhibit each other, expecting behavior in winner takes all, see Figure 3, where the solid line represents positive weights and the dashed line represents negative weights.

**PCTL properties and results** Then we checked two of the most important properties for contralateral inhibition to show that it is well implemented.

$P_4$: $P_>=? [FG(y_2 = 0 \land (F(y_1 = 1)))]$ This specification ensures that in all future times, Neuron 2 stops spiking forever (becomes permanently inactive), and from that point onward, Neuron 1 continues to spike infinitely often, which means Neuron 1 is the winner and takes all priorities.

$P_5$: $P_{>=1}[G > T(y_2 = 0)]$ This specification ensures that in all possible evolutions of the system, after an initial period of T time steps where the system may oscillate, Neuron 2 ceases to spike entirely and remains inactive for all subsequent time.
<figure><img src="image_5.png" /><figcaption>Fig. 3: Contralateral Inhibition</figcaption></figure>

Table 2 shows the outcomes and execution time of $P_4$ and $P_5$.

<table><caption>Table 2: Verification Results of Contralateral Inhibition</caption><thead><tr><th>Properties</th><th>Specifications</th><th>Outcomes</th><th>Time</th></tr></thead><tbody><tr><td>P<sub>4</sub></td><td>P<sub>=?</sub>[F G (y<sub>2</sub> = 0 &amp; (F (y<sub>1</sub> = 1)))]</td><td>1.0</td><td>372 ms</td></tr><tr><td>P<sub>5</sub></td><td>P<sub>&gt;=1</sub>[G &gt; T (y<sub>2</sub> = 0)]</td><td>True (T=100)</td><td>165 ms</td></tr></tbody></table>

Those two properties demonstrate the correctness of our contralateral inhibition model and the fidelity of its biological simulation. These formal guarantees align with empirical observations of contralateral inhibitory circuits in sensory systems, where one neuronal population reliably dominates after mutual competition, thereby validating both the structural integrity and functional realism of our RP-L&IF-based network model.

**Nengo Simulation** Thanks to SNN-RF, we can automatically generate the Nengo RP-L&IF neural network model from identical parameters and topology. For contralateral inhibition, our simulation results illustrate the evolution of each neuron's internal state variables alongside the PRISM model-checking outcomes rendered visually (see Figure 4).

As shown in Figure 4b, Neuron2 emits a single spike at the very start of the simulation and remains silent thereafter. In contrast, in Figure 4a, Neuron1 continues to spike throughout the entire simulation, passing through its active period, normal period, and two refractory periods, with spikes occurring at irregular intervals.
<figure><img src="image_6.png" /><figcaption>Fig. 4: Simulation of Contralateral Inhibition</figcaption></figure>

## 5.3 Convergent Excitatory Circuit

Convergent excitatory circuits integrate multiple inputs to enhance downstream spiking, a mechanism crucial for rhythmic behaviors like locomotion [7,11]. We model such a network with one constant input and two RP-L&IF neurons exciting a postsynaptic target (Fig. 5, solid lines indicate positive weights), to analyze temporal coherence using our framework.

<figure><img src="image_7.png" /><figcaption>Fig. 5: Convergent Excitatory Circuit</figcaption></figure>

**PCTL properties and results** Here we verify three gating and activation properties under different synaptic configurations. Those two properties illustrate different types of convergent excitatory motifs:

$P_6: P_{\ge 1}[(G(y_2 = 0) \land F(y_1 = 1)) \rightarrow F(y_3 = 1)]$ asserts that with probability one, if Neuron 2 remains silent throughout and Neuron 1 spikes at
least once, then Neuron 3 will eventually spike. It guarantees the conditional activation of Neuron 3 by Neuron 1 in the absence of activating input from Neuron 2.

$P_7 : P_{\ge 1}[G((y_1 = 0 \lor y_2 = 0)) \rightarrow \neg F(y_3 = 1)]$ ensures that with probability one, whenever either Neuron 1 or Neuron 2 never spikes, Neuron 3 will never spike. It enforces that a single missing presynaptic activation is sufficient to block downstream firing.

Table 3 shows the results and execution time of $P_6$ and $P_7$.

<table><caption>Table 3: Verification Results of Convergent Excitatory Circuit</caption><thead><tr><th>Properties</th><th>Specifications</th><th>Outcomes</th><th>Time</th></tr></thead><tbody><tr><td>$P_6$</td><td>$P_{\ge 1}[(G(y_2 = 0) \land F(y_1 = 1)) \rightarrow F(y_3 = 1)]$</td><td>True</td><td>9 ms</td></tr><tr><td>$P_7$</td><td>$P_{\ge 1}[G((y_1 = 0 \lor y_2 = 0)) \rightarrow \neg F(y_3 = 1)]$</td><td>True</td><td>1 ms</td></tr></tbody></table>

**Nengo Simulation** In the Nengo part, we simulate two synaptic configurations that satisfy the desired properties, respectively. To better demonstrate our simulation results, here we display the comparisons of spikes of each neuron (see Figure 6).

<figure><img src="image_8.png" /><figcaption>Fig. 6: Simulation of Convergent Excitatory Circuit (the X-axis represents time, and the Y-axis represents spike</figcaption></figure>

Property 6 ensures Neuron 3 activates with just one presynaptic spike, mimicking the brain's reflex-like response to stimuli (Figure 6a). Property 7
requires spikes from both Neuron 1 and Neuron 2 for Neuron 3 to spike, akin to decision-making needing dual sensory inputs (Figure 6b).

# 6 Conclusion and Future Work

SNNs ambition to represent natural neuromorphic computations. Precise representation of basic neuron archetypes' spatiotemporal dynamic (spike timing/probability), as well as of means to combine them into larger brain-like systems, should allow checking how (elementary) properties of the former can contractually ensure more global (stochastic) requirements on the latter, using formal verification (PRISM) for medium-scale proofs and stochastic simulation (Nengo) for large-scale validation.

This paper focuses on the probabilistic temporal specification of individual neuron archetypes. We introduced the RP-LI&F neuron model, unifying discrete-time refractory periods with probabilistic spike generation for biological plausibility. The SNN-RF specification enables automated co-verification across PRISM and Nengo, eliminating toolchain inconsistencies. Case studies on biological archetypes like contralateral inhibition demonstrate preserve neural dynamics with probabilistic formal assurances, validating our co-design approach.

As for future work, the main kind of properties we will want to check are the following contractual requirements: assuming that elementary neuron archetypes are sufficiently alert (in timing and probability of reactive spiking), then the global brain-like neuromorphic computation is guaranteed to satisfy similar reactive constraints. But we want to rely on existing software frameworks to perform these property analyses, namely PRISM and Nengo, and they do not offer such an assume/guarantee contract approach natively. Dealing with the assumption part is rather simple, as it just means to instantiate the parameters to their desired values; note that the SNN-RF format will allow for easy change of such parameter values without affecting the rest of the design specification. Dealing with global requirement constraints is much more involved and largely a matter of future work. Currently, we still write PCTL formulae directly in and for PRISM. The case for Nengo would be to add side-observers running alongside the simulation, and recording spiking test results; the issue then is to provide the number of simulation runs needed (in a Monte-Carlo fashion) to obtain statistically reasonable confidence for our constraint satisfaction.

Finally, based on [3], we intend to propose an algorithm to find parameters such that some key dynamic properties of SNNs are verified in a probabilistic context.

# References

1. Bekolay, T., Bergstra, J., Hunsberger, E., DeWolf, T., Stewart, T.C., Rasmussen, D., Choo, X., Voelker, A.R., Eliasmith, C.: Nengo: a python tool for building large-scale functional brain models. Frontiers in neuroinformatics 7, 48 (2014)
2. De Maria, E., Bahrami, A., l'Yvonnet, T., Felty, A., Gaffé, D., Ressouche, A., Grammont, F.: On the use of formal methods to model and verify neuronal archetypes. Frontiers of Computer Science 16, 1-22 (2022)

3. De Maria, E., Di Giusto, C., Laversa, L.: Spiking neural networks modelled as timed automata: with parameter learning. Natural Computing 19, 135-155 (2020)

4. De Maria, E., Gaffé, D., Ressouche, A., Riboulleau, C.G.: A model-checking approach to reduce spiking neural networks. In: BIOINFORMATICS 2018-9th International Conference on Bioinformatics Models, Methods and Algorithms. pp. 1-8 (2018). https://doi.org/10.5220/0006572000890096

5. DeWolf, T., Jaworski, P., Eliasmith, C.: Nengo and low-power ai hardware for robust, embedded neurorobotics. Frontiers in Neurorobotics 14, 568359 (2020)

6. Fadok, J.P., Krabbe, S., Markovic, M., Courtin, J., Xu, C., Massi, L., Botta, P., Bylund, K., Müller, C., Kovacevic, A., et al.: A competitive inhibitory circuit for selection of active and passive fear responses. Nature 542(7639), 96-100 (2017)

7. Grillner, S.: Biological pattern generation: the cellular and computational logic of networks in motion. Neuron 52(5), 751-766 (2006)

8. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing 6, 512-535 (1994)

9. Hodgkin, A.L., Huxley, A.F.: A quantitative description of membrane current and its application to conduction and excitation in nerve. The Journal of physiology 117(4), 500 (1952)

10. Kabilan, R., Muthukumaran, N.: A neuromorphic model for image recognition using snn. In: 2021 6th International Conference on Inventive Computation Technologies (ICICT). pp. 720-725. IEEE (2021)

11. Kiehn, O.: Decoding the organization of spinal circuits that control locomotion. Nature Reviews Neuroscience 17(4), 224-238 (2016)

12. Koyama, M., Pujala, A.: Mutual inhibition of lateral inhibition: a network motif for an elementary computation in the brain. Current opinion in neurobiology 49, 69-74 (2018)

13. Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23. pp. 585-591. Springer (2011)

14. LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proceedings of the IEEE 86(11), 2278-2324 (1998)

15. Maass, W.: Networks of spiking neurons: the third generation of neural network models. Neural networks 10(9), 1659-1671 (1997). https://doi.org/10.1016/s0893-6080(97)00011-7

16. Maio, V., Lánský, P., Rodriguez, R.: Different types of noise in leaky integrate-and-fire model of neuronal dynamics with discrete periodical input (2004)

17. Sengupta, A., Ye, Y., Wang, R., Liu, C., Roy, K.: Going deeper in spiking neural networks: Vgg and residual architectures. Frontiers in neuroscience 13, 95 (2019)

18. Teeter, C., Iyer, R., Menon, V., Gouwens, N., Feng, D., Berg, J., Szafer, A., Cain, N., Zeng, H., Hawrylycz, M., et al.: Generalized leaky integrate-and-fire models classify multiple neuron types. Nature communications 9(1), 709 (2018)