# A Formal Probabilistic Model of the Inhibitory Control Circuit in the Brain

Elisabetta de Maria, Benjamin Lapijover, Thibaud l'Yvonnet, Sabine Moisan, Jean-Paul Rigault

► To cite this version:

Elisabetta de Maria, Benjamin Lapijover, Thibaud l'Yvonnet, Sabine Moisan, Jean-Paul Rigault. A Formal Probabilistic Model of the Inhibitory Control Circuit in the Brain. BIOINFORMATICS 2023 - 14th International Conference on Bioinformatics Models, Methods and Algorithms, Feb 2023, Lisbonne, Portugal. hal-03999574

HAL Id: hal-03999574

https://inria.hal.science/hal-03999574

Submitted on 21 Feb 2023

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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Formal Probabilistic Model of the Inhibitory Control Circuit in the Brain

Elisabetta De Maria¹, Benjamin Lapijover¹, Thibaud L'Yvonnet², Sabine Moisan² and Jean-Paul Rigault²

Université Côte d'Azur, ¹CNRS, I3S, Sophia Antipolis, France, ²INRIA, Sophia Antipolis, France
elisabetta.de-maria@univ-cotedazur.fr, benjamin.lapijover@etu.univ-cotedazur.fr, {firstname.lastname}@inria.fr

**Keywords:** Inhibitory Control, Biological Neural Networks & LI&F model, Probabilistic Model, Model Checking.

**Abstract:** The decline of inhibitory control efficiency in aging subjects with neurodegenerative diseases is due to anatomical and functional changes in (pre)frontal regions of the brain. Among these regions, the basal ganglia play a central role in the inhibitory control loop. We propose a probabilistic formal model of the biological neural network governing the inhibitory control function and we study some of its relevant dynamic properties. We also explore how parameter variations influence the probability for the model to display some key behaviors. We model the different structures of the inhibitory control loop thanks to discrete Markov chains representing Leaky Integrate and Fire neurons. The model is implemented and verified using the PRISM framework. The final aim is to detect sources of pathological behaviors in the neural network responsible for inhibitory control.

## 1 INTRODUCTION

This work proposes a formal model of the neural network governing the inhibitory control function of the human brain and studies some of its dynamic properties. We chose this function because it has been studied for a long time and several models already exist (Verbruggen and Logan, 2009); moreover, it is managed by a restricted amount of brain structures (basal ganglia) which makes it easier to model than other cognitive functions. The aim is to artificially represent the behavior of inhibitory control in humans through a probabilistic model. The main advantage of probabilistic models is their ability to represent a wide variability of behaviour with a single model. In the context of early onsets of neuropathologies, this approach is convenient as even healthy subjects are not necessarily expected to ace clinical tests. We model the different structures involved in the inhibitory control loop thanks to probabilistic discrete Markov chains implementing a modified version of *Leaky Integrate and Fire* neurons. Markov chains are widely used in biology, especially for modeling event driven probabilistic systems. In the case of neurobiology, there have been various utilizations of Markov chains to simplify neurons modeling (Sakumura et al., 2001; Nossenson and Messer, 2010; Inoue et al., 2021). We rely on formal methods to implement this model and on *model checking* techniques to validate

and explore it. More precisely, we use PRISM (a state of the art probabilistic model checker) to implement the model and to perform model checking.

## 2 FORMAL MODELING AND VERIFICATION

Model checking is a method developed in the eighties (Clarke et al., 1986) for automatic verification of software models. It helps identify software design problems before implementation. In our case, we use model-checking not to verify a software tool, but to model the functioning of a brain structure and to explore all its possible behaviors. Hence probabilistic models are well adapted.

Among the existing probabilistic model checkers, we chose PRISM (Kwiatkowska et al., 2011) which is well established in the literature, and compatible with many other tools (parameter synthesis tools or other model checkers). PRISM is a tool for formal modeling and analysis of systems with random or probabilistic behavior. It supports several types of probabilistic models, discrete as well as continuous.

For the modeling formalism, we rely on discrete-time Markov chains (DTMCs), which are transition systems augmented with probabilities. Their set of states represents the possible configurations of the
modeled system and the transitions between states represent the evolution of the system, which occurs in discrete-time steps. Probabilities to transit between states are given by discrete probability distributions.

The dynamics of DTMCs can be specified thanks to the PCTL\* (Probabilistic Computation Tree Logic) temporal logic (Hansson and Jonsson, 1994). The main PCTL\* state quantifiers that we use in this paper are **X** (next time), **F** (sometimes in the future), **G** (always in the future). The until operator, **U**, is such that *p1 U p2* means that property *p1* remains *true* until property *p2* becomes *true*.

The most important PCTL\* operator is **P**, to reason about the probability of event occurrences. **P** is used to replace the usual path quantifiers *forall* and *exists*. A property *P bound [prop]* is true in a state *s* if the probability that property *prop* holds in all the paths from *s* satisfies the bound *bound* (a comparison operator followed by a probability value). For example, the property *P= 0.5 [X (y = 1)]* holds in a state if the probability that *y* = 1 is true in the next state equals 0.5. All the above state quantifiers, except **X**, have bounded variants, where a time bound is imposed on the property. Furthermore, the **P PRISM** operator can be used as *P=? [prop]* to compute the probability for *prop* to occur.

PRISM also supports positive real value user-defined "rewards" which can be seen as counters that do not impact the number of states and transitions of the model nor its behavior. The **R** operator allows to retrieve reward values. Additional operators deal with reward: we mainly use **C** (cumulative-reward). PRISM model checking algorithms automatically validate DTMCs over PCTL\* or reward-based properties. They compute the actual probability of some behavior of a model to occur. In addition, PRISM offers the possibility to run *experiments* which is a "way of automating multiple instances of model checking" according to its authors. This feature allows users to obtain curves displaying the evaluation results of a property with respect to one or several variables. Besides, PRISM also proposes *statistical model-checking*, a way to test properties through several simulations.

# 3 COGNITIVE FUNCTIONS AND BRAIN STRUCTURES

Cognitive functions is a broad designation for brain
processes necessary in the acquisition and process-
ing of information and in reasoning (e.g., learning,
awareness, decision making (Kiely, 2014)). The con-
cept of cognitive functions is the base of many exist-
ing models of the brain mechanisms. For instance, J.

Hopfield modeled the associative memory with neural
networks (Hopfield, 1982). More recently, (Schmidt
et al., 2019) used artificial neuron models to under-
stand the relations between the brain waves and cog-
nitive functions such as working memory or executive
control. One of the main challenges of neurocognitive
science is to better understand the cognitive functions
and their interactions, which may improve the clinical
assessment methods and the therapies.

**3.1 Biological Neuron**

Biological neurons allow inter cellular communica-
tion via electrical signals. They can have thousands
of ramifications called dendrites that receive nerve
(sensory and motor) information, named *afferent sig-
nals*. On the other hand the axon is usually unique and
sends information (*efferent signals*) to other cells.

The *action potential* that runs through the axon is a nerve impulse caused by the difference in ion concentration between the inside and the outside of the neuron. When a neuron does not receive any signal, the membrane maintains a resting potential which constantly balance the concentration of the potassium ions on both sides of the membrane. Nerve impulses modulate the membrane potential and if this potential exceeds the threshold of excitability it triggers in turn an *action potential* (a.k.a. *spike*). A spike is a quick rise and fall of the membrane potential. It travels along the neuron axon to reach the synaptic terminals (Purves et al., 2019). Depending on the emitting neuron, the spike either directly travels to the dendrites of the receiving neurons or triggers the release of neurotransmitters. These neurotransmitters reach receptors on the dendrite side of the synaptic connection. In both cases, the receiving neuron follows the same cycle as the neuron that sent the spike.

**3.2 Inhibitory Control Circuit**

According to the literature (Jahanshahi et al., 2015), the brain regions involved in the inhibitory control cognitive function are the cortex, the basal ganglia, and the thalamus. Together, these anatomical structures make it possible to temporarily stop the action of the motor cortex and therefore to inhibit an irrelevant action initially planned. A deficit in this circuit can cause cognitive impairment (Braak et al., 2002).

The basal ganglia (figure 1) are considered as motor structures that allow movements to start and stop. Basal ganglia are essentially a part of the *motor loop* and thus of the inhibitory control circuit. They contain several anatomical structures such as the *striatum* (STr), composed of the putamen and caudate nu-
cleus. These two latter structures are distinct in the circuit, but in our formal model we only represent the STr. This simplification is advisable to limit the size and complexity of the model and acceptable because the striatum can be considered as a whole functional zone (Johns, 2014). Basal ganglia also contain the globus pallidus separated into two structures: the outer segment Gpe and the inner segment Gpi (related to the substantia nigra pars reticulata noted SNpr, that we represent together in our model); the subthalamic nucleus (STN); and the substantia nigra pars compacta (SNpc). The cortex (Cx) and the thalamus (Th) are also part of the inhibitory control loop but not of the basal ganglia (Purves et al., 2019).

<figure><img src="image_2.png" /><figcaption>Figure 1: Brain coronal section of basal ganglia and its components (from A. Gillies, M. Häggström & P. J. Lynch).</figcaption></figure>

There are two pathways in the inhibitory control loop. In the direct pathway, after receiving inputs from the cortex, specialized STr neurons target specific neurons of the Gpi/SNpr complex with inhibitory inputs (Mink, 1996). These inputs trigger the disinhibition of the Th area, controlling the expression of the desired motor program, leading to "release" (Graybiel, 2000) the intended physical movement. In the indirect pathway, STr neurons target the Gpe with inhibitory inputs leading to the disinhibition of STN. At the same time, STN specialized neurons receive powerful afferent signals from the cortex (Purves et al., 2019) and target the Gpi/SNpr complex with excitatory inputs (Mink, 1996). These inputs trigger the inhibition of Th (Graybiel, 2000) in a way that removes all the unwanted motor programs.

The decline of inhibitory control efficiency in aging subjects is due to anatomical and functional changes in (pre)frontal regions (Hu et al., 2014). However, there are differences between healthy and pathological aging. One of our goals is to differentiate these two conditions. It has been shown (Crawford et al., 2005) that in neurodegenerative diseases, such as Parkinson's disease, there is a degeneration of the neurons of the substantia nigra pars compacta (SNpc). The dopaminergic influx coming from the SNpc and targeting STr is considerably reduced. STr is then less inhibited which consequently reduces the inhibitory emission of the basal ganglia, removes the inhibition of the thalamus and therefore the motor inhibition.

# 4 COMPUTATIONAL MODELING

## 4.1 Inhibitory Control Models

Several models of the inhibitory control use the go/no-go task to study and describe its underlying mechanisms, for example, the horse-race models reviewed in (Verbruggen and Logan, 2009). They see the inhibitory control function as a competition between a "go" and a "stop" process in the brain. This modeling approach gave many insights on the mechanisms of the inhibitory control (Schall and Godlove, 2012). With the rise of computational simulation techniques, the past decades have seen the development of models based on neural networks with respect to neuroanatomy (Schroll and Hamker, 2013).

The model presented in this work is inspired by the work of (Wei and Wang, 2016) which attempted to model the inhibitory control function with a set of (heavy) biological "Leaky Integrate and Fire" neuron networks representing each brain structure involved in this function.

## 4.2 Artificial Neural Network Models

The *Leaky Integrate and Fire* (LI&F) model is a good compromise between biological fidelity and computational efficiency for mathematical analysis (Izhikovich, 2004).

### 4.2.1 Leaky Integrate and Fire Discrete Model

According to the LI&F model, the membrane of a neuron can be represented as an electronic circuit (Brunel and Van Rossum, 2007). In this model the intensity of the action potential is neglected, but the instant of its occurrence plays an important role (Paugam-Moisy and Bohte, 2012). We consider a discrete version of the model where the membrane potential $u$ at time $t$ is defined by

$$u(t) = \begin{cases} \sum_{i=1}^{n} w_i \cdot x_i(t) + r \cdot u(t-1) & \text{if } u(t-1) < \text{Tau} \\ \sum_{i=1}^{n} w_i \cdot x_i(t) & \text{otherwise} \end{cases}$$

where $x_i(t) \in \{0,1\}$ is the signal received at time $t$ by the neuron through its $i^{th}$ input synapse; $w_i$ is the weight associated with the $i^{th}$ input synapse; $r$ is the leak factor; $\text{Tau}$ is the excitability threshold beyond which the neuron emits an action potential. If the membrane potential at time $t$ exceeds the threshold, a spike is emitted and the membrane potential is reset to zero. The neuron output function $s(t) \in \{0,1\}$ is therefore defined by

$$s(t) = 1 \text{ if } u(t) \geq \text{Tau}, 0 \text{ otherwise}$$
### 4.2.2 Generalization to Neuron Boxes

Our goal is to model the interactions of structures of the brain (made of thousands of neurons) while keeping model checking tractable. As modeling each and every neurons would make the model difficult to check, we introduce a generalization of the LI&F neuron to neuron *boxes*. We modified the equation of the LI&F neuron to represent several neurons, each one producing its own output at a given instant.

Each anatomical structure of the inhibitory control circuit is represented by a box of ten neurons of LI&F type. This number is not proportional to the actual number of neurons in the brain structures. It is a trade off between biological accuracy and computation capacity: the model checking experiments (see 5.4) show that this simplification is realistic enough to represent these brain structures. Indeed, a network of ten neurons cannot mimic the behavior of complex networks with thousands of neurons. However, it shows a "firing ratio" (number of firing neurons out of the ten ones) for each time step. Moreover, the generalization allows to model these ten neurons with only one entity that directly computes the firing ratio at each time step. Thus boxes makes it possible to have a behavior relatively close to a small network of neurons, without requiring a lot of computing power.

To take into account the difference of sizes between biological structures, the weight of each connection of the model was set to a value proportional to the weight of the same connection and the number of neurons connecting two structures in the model of Wei and Wang. The dynamic of a box is defined by:

$$U(t) = \sum_{i=1}^{n} w_i \cdot X_i(t) + r \cdot U(t-1) \cdot \left( \frac{N-S(t-1)}{N} \right)$$

This formula is close to the usual LI&F one (see section 4.2.1) except that Boolean $x_i$ is replaced by integer $X_i$ ranging from 0 to 10 to mimic the possible 10 neuron inputs from another box. Another simplification is that when a biological connection exists between two boxes A and B, all neurons of box A are considered to be connected to all neurons of box B.

Thus, the new formula does not take Boolean inputs but input firing ratio. This simplification led to a new parameter, $N$, that represents the number of neurons in the whole box ($N = 10$ in the presented model). As neurons are far less sensitive to stimuli after emitting a spike due to the "refractory periods" (Purves et al., 2019), the last term of the formula was introduced. In this term, $S(t-1)$ represents the number of neurons which discharged at the previous time step. More precisely, $S(t)$ is defined by

$$S(t) = \frac{U(t)}{\text{Tau}}, \text{ where } 0 \le S(t) \le N$$

To track the activity of a box in the model, one should check the values of $S(t)$ of this box in the time window of interest.

Since biological inputs from the cortex are irregular, the input spikes are modeled by a Poisson law (Heeger, 2000). To approximate this irregularity, Wei and Wang modeled these inputs as Poisson spike trains. Our model uses the same Poisson function to compute the activation probabilities of the cortex and SNpc neurons: $P(k) = \frac{e^{-\lambda}\lambda^k}{k!}$, where $k$ is the number of cortex and SNpc neurons that send a spike.

# 5 MODEL AND VALIDATION

The first task was to provide a formal model of the main interactions between the different basal ganglia nuclei. We developed a PRISM model to artificially mimic the behavior of human inhibitory control through a probabilistic model based on discrete-time Markov chains. Second, we automatically tested probabilistic temporal properties of this model thanks to model-checking to explore potential sources of pathological behavior in the inhibitory control circuit. The complete code of the model and supplementary materials can be found at https://gitlab.com/ThibLY/inhibctrlformmodel.git.

## 5.1 Basal Ganglia Model Overview

Neuropsychologists and neurobiologists have theorized several models of the functioning of the basal ganglia which have already been integrated into software systems. In (Wei and Wang, 2016) the authors proposed a neural network model of LI&F neurons for the functional structures of the basal ganglia. They obtained diagrams to visualize e.g., the importance of some specific connections in inhibitory control.

We keep the same division into functional structures. As mentioned, we mainly use model checking techniques that allow the automated exploration of each state of a model to validate or to reject a given property. However, these methods imply to implement models with lower complexity than simulation methods. Thus, our model follows the architecture of Wei and Wang using LI&F neuron boxes and other adaptations, resulting in the graph of figure 2.

The PRISM code for a single box of neurons follows the formula in section 4.2.2. We added conditions to limit the output firing ratio of boxes to values between 0 and 10 as each box represents 10 neurons (see figure 3). The whole model contains all the biological structures represented in the basal ganglia square of figure 2 plus the thalamus. We introduced
<figure><img src="image_3.png" /><figcaption>Figure 2: Inhibitory control circuit diagram. In green: direct pathway, in red: indirect one. A classic arrow corresponds to an excitation, a flat-tipped arrow to an inhibition.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 3: Example of PRISM code of a box of neurons receiving inputs from another box and the inputs of the model.</figcaption></figure>

excitatory and inhibitory connections between them and we add connections from the cortex as inputs; these inputs follow a Poisson law determining the number of spikes sent to the STr and Th boxes (section 4.2.2). Finally, we implemented an additional *Delay* box between the STN and the SNpr boxes to enforce a discrete loop and we integrated alternative connections between the SNpc and STr to differentiate a healthy brain from a brain with a degenerated SNpc. For this we defined 2 different formulas (see PRISM code in figure 4): one takes into account both the SNpc and the cortex inputs and the second one only takes inputs from the cortex. Since (Cheng et al., 2010) showed that the death of dopaminergic neurons reaches 70% in the later phases of Parkinson's disease, we considered that a pathological brain has a 30% probability to follow the first formula and a 70% probability to follow the second. In a healthy brain, dopaminergic neurons are functional so the

brain model will always follow the first formula.

## 5.2 PRISM Model Implementation

The model was implemented and verified with the PRISM framework. Each neuron box is implemented by one PRISM module. All the neuron box modules have a common structure with two variables (for global membrane potential and firing ratio) and one set of *guards* and *updates*.

### 5.2.1 Healthy Inhibitory Control Model

The implementation in PRISM of a healthy inhibitory control contains six modules: *Entry* (partial representation of cortex and SNpc), STr, GPe, STN, SNpr (representing the Gpi/SNpr complex considered as a single functional structure), and Th. These modules have an associated formula for their global membrane potential and constants for their connection weights, except *Entry* that generates input spikes following a Poisson law. Their connections follow the architecture of the basal ganglia shown in figure 2. However, we add two modules. First, the *Delay* module is a simplified neuron box that sends the same amount of spikes that it receives but at the next instant. This supplementary module is necessary as our model is a discrete system. It allows the SNpr to receive signals from GPe and STN simultaneously, by delaying signals from STN to make them reach SNpr at the same instant as the ones from GPe. Second, the *Inhibitor* module generates no-go signals at regular intervals (every ten counts) to simulate external inhibitory events. In the model, it sends *stop* signals to the *STN* module. As shown in figure 2, the *Th* module receives the final inhibition signal; hence, if its output firing ratio is low, it indicates a successful inhibition.

### 5.2.2 Parkinsonian Inhibitory Control Model

To model the behavior observed in Parkinson's disease, we proposed an alternative formula for the global membrane potential of STr (see figure 4). The STr neuron box module has one more update in its set of guards and updates. It has a probability of 0.3 to update its membrane potential with the "healthy" formula and of 0.7 to update it with the "pathological" one, according to (Cheng et al., 2010).

## 5.3 Properties of Individual Boxes and of Box Synchronization

The first step was to validate the boxes individually. Each neuron box must respect the specifications
<figure><img src="image_5.png" /><figcaption>Figure 4: Code excerpt: brain with Parkinson syndrome.</figcaption></figure>

stated in section 4.2.2. In particular, at the box level, the model must verify the conditions concerning the global membrane potential and the firing ratio: the maximum and minimum global membrane potential must not be exceeded; the maximum and minimum number of spikes must be respected; as long as the global membrane potential is not greater than or equal to a threshold, there should be no spike. Thus, we verified that the corresponding PCTL* properties, which are invariants of the boxes, hold for all boxes. In the property below, X denotes the current box under test, n_X is the number of spikes emitted by box X, and potential_X is the global membrane potential of X. As a reminder, P =? is the PCTL operator to compute a probability and F = nprop indicates whether property prop is true at time step n.

**Property 1.** What is the probability for the number of spikes to always be 0 until the potential equals or exceeds tau = 80?

$$P =? [n_X = 0 \cup potential_X \geq 80]$$

The resting potential of a neuron is -10mV and the biological threshold is 70mV; since the resting potential in our model is 0 we chose a threshold value of 80. The PRISM model checker gives a positive answer (P=1) for all properties and all boxes.

The next step is to validate the synchronization of the boxes which must be connected to respect the known properties about the connections of the corresponding biological structures, as shown in figure 2. As examples, the next properties check both the direct and indirect pathways from the instant the stop signal is sent (arbitrarily chosen to be the tenth).

**Property 2.** What is the probability for the stop signal to rise at the 10th instant?

$$P =? [F = 10 \ n\_STN > 3]$$

**Property 3.** What is the probability for GPe and the

Delay box to be activated at the 11th instant?

$$P =? [F = 11 \ n\_GPe > 3 \ \& \ n\_Delay > 3]$$

**Property 4.** What is the probability for STr to be inhibited and SNpr to be activated at the 12th instant?

$$P =? [F = 12 \ n\_STr < 5 \ \& \ n\_SNpr > 3]$$

PRISM explicit model checking engine gives the expected valid answers (P=1). The model shows the disinhibition and activation of Gpi/SNpr nuclei that trigger the inhibition of the thalamus and thus the inhibition of an action. Moreover, the simulation graph in figure 5 (obtained with the "run experiment" and statistical model-checking tools of PRISM) showing spiking activity also confirms the inhibition of STr and Th following a stop signal. Though they are not at the same scale level, these activities can approximate the simulation results of (Wei and Wang, 2016).

<figure><img src="image_6.png" /><figcaption>Figure 5: STN-SNpr-Th path. The stop signal reaches the STN, enables the SNpr activation (through the STr inhibition at the same time (t = 13)), and finally the thalamus inhibition, and therefore of the behavioral response; in red: STN, in blue: SNr, in green: Th.</figcaption></figure>

## 5.4 Property on Thalamus Inhibition

To deduce the probability that a movement is actually inhibited, we defined a property evaluating the probability to observe a low number of firing neurons in the thalamus box. We arbitrarily consider that the Th box is inhibited when it releases less than 4 spikes (40% of the maximal "firing ratio" which is 10 in our implementation). In PCTL* this property is written:

**Property 5.** What is the probability for Th to be inhibited at the first stop trial (13th time-step)?

$$P =? [F = 13(n\_Th < 4)]$$

We compared our model checking results with the simulation results of Wei and Wang. The behavior of our formal inhibitory control model is close to the results presented in (Wei and Wang, 2016). This behavior is still described as a race in which the stop signal
information has to transit from STN to SNpr before the STr inputs inhibit SNpr (Schmidt et al., 2013).

Wei and Wang conducted an experiment on their model by modulating the network weights. The goal was to determine if the inhibitory control behavior is more sensitive to the modulation of some connections than to others. To reproduce this experiment on our model, we doubled the weight of all the connections one at a time and we computed the probability to reach a state where the number of spikes emitted by the thalamus is less than 4. The results, shown in figure 6, go slightly beyond those of (Wei and Wang, 2016). In this figure a + indicates that increasing the

<figure><img src="image_7.png" /><figcaption>Figure 6: Inhibitory control circuit with modification of connection weights.</figcaption></figure>

weight of the associated connection increases the *Stop Signal Reaction Time* (SSRT) (lower probability for Th inhibition), and a – indicates that increasing the weight decreases SSRT (higher probability for Th inhibition). This experiment highlights two categories of connections: those which facilitate thalamus inhibition and those which prevent it. The STr-GPe, STN-SNpr, and SNpr-Th connections belong to the first category while GPe-GPe, STN-GPe, Gpe-SNpr, and STr-SNpr connections belong to the second one (see figure 6). To the best of our knowledge these specific connections are yet to be studied *in vivo*. Such results need further biological experiments for validation.

<table><caption>Table 1: Model checking results (explicit engine) for property 5 of the model without modifications (Original) and after weight modification of specific connections.</caption><thead><tr><td>Connection</td><td>Result</td><td>Time (s)</td></tr></thead><tbody><tr><td>Original</td><td>0.8527</td><td>0.288</td></tr><tr><td>Gpe-SNpr</td><td>0.5251</td><td>0.303</td></tr><tr><td>STr-SNpr</td><td>0.4889</td><td>0.300</td></tr><tr><td>STr-GPe</td><td>0.9432</td><td>0.310</td></tr><tr><td>STN-SNpr</td><td>1</td><td>0.267</td></tr><tr><td>SNpr-Th</td><td>1</td><td>0.250</td></tr></tbody></table>

Table 1 shows results and computation times for the verification of property 5 for the model with-

out modification and for some connection modifications. The decrease of the number of firing neurons in the STr-GPe, STN-SNpr, and SNpr-Th connections causes a decrease in the probability of inhibition and consequently a decrease in behavioral inhibition. A decrease in the inhibition probability in the model means a longer SSRT leading to the fulfillment of an unwanted action. More bibliographical research may be necessary to evaluate the relevance of these results.

## 5.5 Comparison of Impaired versus Healthy Brain Models

In a healthy brain all SNpc neurons are present. As the number of SNpc neurons depletes in Parkinson's disease (Cheng et al., 2010), with about 30% neurons remaining in SNpc of advanced Parkinson's, an unhealthy brain only has 30% probability of taking SNpc neurons into account. Still with property 5 we

<table><caption>Table 2: Results of property 5 for the model without modifications (Healthy) and the Parkinsonian model.</caption><thead><tr><td></td><td>Result</td><td>Time (s)</td></tr></thead><tbody><tr><td>Healthy</td><td>0.8527</td><td>0.288</td></tr><tr><td>Parkinson</td><td>0.7651</td><td>2.42</td></tr></tbody></table>

found that there is a greater chance of getting a thalamus inhibition in the case of a healthy brain (table 2). The second formula in figure 4 and its associated 30% probability are enough to lead to smaller chances of action inhibition (of the order of $10^{-1}$).

## 6 CONCLUSION AND PERSPECTIVES

A better understanding of the mechanisms of inhibitory control could allow targeted treatments for different classes of patients with dementia. This work proposed a discrete probabilistic model of the inhibitory control circuit of the brain and its formal validation. This model reproduces known biological behaviors from the literature such as the pathway race. Our model also faithfully represents the importance of some connections in the pathways (e.g., SNr and STr connections). These behaviors were translated in PCTL properties to check the adequacy of the model. We also ran an experiment to explore the sensitivity of inhibitory control to the modulation of some connections. The modified model complies with Parkinson's disease. Further modifications to represent, e.g., Alzheimer's disease are planned as future work.

Probabilistic formal models can represent a wide variety of behaviors while enabling model checking.
To check our model with standard tools, it was necessary to brought up a new generalization of the LI&F classical neuron model to represent small networks behavior with a single module. This work opens new avenues for the formal modeling of cognitive functions. Moreover, it has proven the feasibility of such model exploration using only off the shelf laptops.

In the future, the model will be coupled with the activity model of a patient playing a serious game targeting the inhibitory control function. The goal is to explore modifications in the brain neural network that may generate a patient behavior characteristic of neurocognitive disorders.

## REFERENCES

Braak, H., Tredici, K. D., Bratzke, H., Hamm-Clement, J., Sandmann-Keil, D., and Rüb, U. (2002). Staging of the intracerebral inclusion body pathology associated with idiopathic Parkinson's disease (preclinical and clinical stages). *Journal of Neurology*, 249.

Brunel, N. and Van Rossum, M. C. (2007). Lapicque's 1907 paper: from frogs to integrate-and-fire. *Biological cybernetics*, 97.

Cheng, H. C., Ulane, C. M., and Burke, R. E. (2010). Clinical progression in Parkinson disease and the neurobiology of axons. *Annals of Neurology*, 67.

Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. *ACM Transactions on Programming Languages and Systems (TOPLAS)*.

Crawford, T., Higham, S., Renvoize, T., Patel, J., Dale, M., Suriya, A., and Tetley, S. (2005). Inhibitory control of saccadic eye movements and cognitive impairment in Alzheimer's disease. *Biological Psychiatry*, 57.

Graybiel, A. M. (2000). The basal ganglia. *Current biology*, 10.

Hansson, H. and Jonsson, B. (1994). A logic for reasoning about time and reliability. *Formal aspects of computing*.

Heeger, D. (2000). Poisson model of spike generation. *Handout, University of Standford*, 5.

Hopfield, J. J. (1982). Neural networks and physical systems with emergent collective computational abilities. *Proceedings of the national academy of sciences*, 79.

Hu, S., Chao, H. H.-A., Zhang, S., Ide, J. S., and Li, C.-S. R. (2014). Changes in cerebral morphometry and amplitude of low-frequency fluctuations of bold signals during healthy aging: correlation with inhibitory control. *Brain Structure and Function*, 219.

Inoue, H., Hukushima, K., and Omori, T. (2021). Estimation of Neuronal Dynamics of Izhikevich Neuron Models from Spike-Train Data with Particle Markov Chain Monte Carlo Method. *Journal of the Physical Society of Japan*, 90.

Izhikevich, E. M. (2004). Which model to use for cortical spiking neurons? *IEEE transactions on neural networks*, 15.

Jahanshahi, M., Obeso, I., Rothwell, J. C., and Obeso, J. A. (2015). A fronto–striato–subthalamic–pallidal network for goal-directed and habitual inhibition. *Nature Reviews Neuroscience*, 16.

Johns, P. (2014). Chapter 3 - functional neuroanatomy. In Johns, P., editor, *Clinical Neuroscience*. Churchill Livingstone.

Kiely, K. M. (2014). Cognitive function. In Michalos, A. C., editor, *Encyclopedia of Quality of Life and Well-Being Research*. Springer Netherlands, Dordrecht.

Kwiatkowska, M., Norman, G., and Parker, D. (2011). PRISM 4.0: Verification of probabilistic real-time systems. In *Proc. 23rd Int. Conf. on Computer Aided Verification (CAV'11)*.

Mink, J. W. (1996). The basal ganglia: Focused selection and inhibition of competing motor programs. *Progress in Neurobiology*, 50.

Nossenson, N. and Messer, H. (2010). Modeling neuron firing pattern using a two state markov chain. In *2010 IEEE Sensor Array and Multichannel Signal Processing Workshop*.

Paugam-Moisy, H. and Bohte, S. M. (2012). Computing with spiking neuron networks. *Handbook of natural computing*, 1.

Purves, D., Augustine, G.-J., Fitzpatrick, D., and Hall, W. (2019). *Neurosciences*. Broché.

Sakumura, Y., Konno, N., and Aihara, K. (2001). Markov chain model approximating the hodgkin-huxley neuron. In Dorffner, G., Bischof, H., and Hornik, K., editors, *Artificial Neural Networks — ICANN 2001*, Berlin, Heidelberg. Springer Berlin Heidelberg.

Schall, J. D. and Godlove, D. C. (2012). Current advances and pressing problems in studies of stopping. *Current Opinion in Neurobiology*, 22. Decision making.

Schmidt, R., Herrojo Ruiz, M., Kilavik, B. E., Lundqvist, M., Starr, P. A., and Aron, A. R. (2019). Beta oscillations in working memory, executive control of movement and thought, and sensorimotor function. *Journal of Neuroscience*, 39.

Schmidt, R., Leventhal, D. K., Mallet, N., Chen, F., and Berke, J. D. (2013). Canceling actions involves a race between basal ganglia pathways. *Nature neuroscience*, 16.

Schroll, H. and Hamker, F. (2013). Computational models of basal-ganglia pathway functions: focus on functional neuroanatomy. *Frontiers in Systems Neuroscience*, 7.

Verbruggen, F. and Logan, G. D. (2009). Models of response inhibition in the stop-signal and stop-change paradigms. *Neuroscience & Biobehavioral Reviews*, 33. Translational Aspects of Stopping and Response Control.

Wei, W. and Wang, X.-J. (2016). Inhibitory control in the cortico-basal ganglia-thalamocortical loop: Complex regulation and interplay with memory and decision processes. *Neuron*, 92.