# On Model Reductions of Boolean Networks

Claudine Chaouiya, Jerome Feret, Patricia Roxo

► To cite this version:

Claudine Chaouiya, Jerome Feret, Patricia Roxo. On Model Reductions of Boolean Networks. 23rd International Conference on Computational Methods in Systems Biology, CMSB 2025, François Fages; Sabine Peres, Sep 2025, Lyon, France. pp.19, 10.1007/978-3-032-01436-8_3. hal-05115042

HAL Id: hal-05115042

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

Submitted on 20 Aug 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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Model Reductions of Boolean Networks

Claudine Chaouiya¹[0000-0003-2350-0756], Jérôme Feret²[0000-0002-2601-2785],
and Patrícia Tenera Roxo¹,²

¹ Aix-Marseille Université, CNRS, I2M, Marseille, France

² DI ENS, École Normale Supérieure, PSL, CNRS, INRIA, Paris, France

**Abstract.** Boolean networks are a class of qualitative models used extensively to model regulatory interactions driving biological processes. While structurally simple, their dynamics can be quite complex. One recurrent issue in studying the dynamics of these models is state explosion. To tackle this problem model reduction techniques are employed. These techniques aim at producing smaller models that behave approximately as the original model.

In this paper, we use Abstract Interpretation, a unifying framework to compare semantics of models at different levels of abstraction. Here, we relate the behaviors of the initial and reduced models for two model reduction approaches, a new method and the classical one proposed by Naldi *et al*. In both cases, we formally characterize which traces are preserved by construction.

**Keywords:** Boolean Networks · Abstract Interpretation · Model Reduction · Reachability.

## 1 Introduction

The Boolean formalism has long been proposed to assess the dynamical properties of complex regulatory networks [23,14,24]. Since then, the framework has evolved significantly, notably, through the adoption of the asynchronous update scheme and the extension to multi-valued variables [26,25]. Boolean modeling has proven to be well-suited to capture the complexity of gene regulatory and signaling networks (see, e.g., [27,3]). The evolution of Boolean modeling has led to both theoretical advances and the development of dedicated modeling tools.

A Boolean model of a regulatory network with $n$ components defines its evolution over the $2^n$ possible states. Properties of interest relate to the attractors of the model (fixed points or cyclical behaviors), which embody e.g. cellular phenotypes or responses to external stimuli [3]. In addition to identifying these attractors, it is often essential to assess their reachability properties. Expectedly, the analysis of such properties is hampered by the size of the state space for large networks. To address this issue, Naldi *et al.* proposed a reduction method [15,16] for regulatory networks. This reduction is quite natural, as it consists in removing an intermediate component between two components that are then directly connected. It proved useful to assess the dynamics of
large models (see, e.g., [13]) and has been implemented in the modeling software GINsim [18]. It is also available in the CoLoMoTo Interactive Notebook [19] (https://colomoto.github.io/colomoto-docker/) through the Java BiLQM programming interface [17]. It has been shown that any trace in the reduced model obtained by applying Naldi's reduction corresponds to an existing trace in the original model [16]. However, for a reduced model, if a given reachability property is not satisfied, one cannot conclude that this property is not satisfied either in the original model. The main motivation of this work is to address this issue by proposing a reduction method that ensures that any trace in the reduced model has a counter-part in the original model.

We revisit both model reductions using Abstract Interpretation, a unifying framework to formally relate the behaviors of a dynamical system at different levels of observation [6]. Abstract Interpretation has been used to reduce the semantics of reaction networks to logical models in [1,2]. This abstraction is refined in [11] to recover information about the probability distribution of transitions in the reduced (logical) model. In [7], it is used to relate the stochastic and Boolean semantics of BIOCHAM. In [21], Abstract Interpretation is applied to derive sound under- and over-approximation of the behavior of systems that are written in the Process-Hitting formalism. This analysis has been extended to autotaton networks in [12]. In the context of model reduction of rule-based models, an exact reduction of the differential (resp. stochastic) semantics of the Kappa language can be obtained based on tracking information flow [9] (resp. [10]), or by studying symmetries [9] (for both semantics). Numerically approximate abstractions of the differential semantics of Kappa have also been formally derived based on time-scale separation [4] and truncation of numerical series [8]. Both provide guaranteed error bounds.

We begin this paper with Section 2 by introducing the necessary foundations of Boolean Networks and Abstract Interpretation. Section 3 then presents a new trace-preserving reduction technique, first defined syntactically and subsequently derived semantically by means of Abstract Interpretation. Section 4 abstracts the dynamics of a Boolean Network based on the time-scale separation principle that establishes that a given component of the system evolves incomparably faster than the remaining. We show that the well-known reduction proposed by Naldi *et al.* emerges as a special case of this abstraction. The paper concludes with some final remarks and future prospects in Section 5.

# 2 Background and Notation

## 2.1 Boolean Models

A Boolean Network (BN) model over $n$ components is defined by a set of functions, often called *regulatory functions*, $f = \{f_i\}_{i=1}^n$. Each $f_i: \mathbb{B}^n \to \mathbb{B}$ encodes how the value of component $i$ evolves depending on the current state of the network. These functions define a regulatory network embodying signed influences between model component [3]. The dynamics of a model is defined with respect to a fixed update scheme. The dynamics can be represented by means of a State
Transition Graph (STG) where each node is a state of the model and directed edges between states denote that the model can evolve from the source state to the target state. The STG thus captures all possible behaviors of the model, with each trace of the STG representing one such behavior.

Among the many existing update schemes, the asynchronous one is usually preferred. Its underlying assumption is that no two events can occur exactly at the same time. Thus under the asynchronous update scheme, any transition in the STG of a model updates exactly one component. When an STG complies with this condition we say it is *well-defined*. Throughout this paper we adopt exclusively the asynchronous update scheme and equate STGs to sets of transitions.

**Definition 1 (Basic Objects).** The state space of a BN over n components is $\mathbb{B}^n$. A state is an element $s \in \mathbb{B}^n$. A transition is an ordered pair of states, $\langle x, y \rangle \in \mathbb{B}^n \times \mathbb{B}^n$. A finite trace is any k-tuple of states, $\langle s_1, \dots, s_k \rangle \in (\mathbb{B}^n)^k$. An STG is a set of transitions. The set of all n-dimensional STGs is denoted by $S_n$. The set of all finite traces is denoted by $\mathcal{T} = (\mathbb{B}^n)^*$, the Kleene closure of $\mathbb{B}^n$. The set of all transitions is denoted by $\mathcal{T}_2$, the subset of traces of length two.

When analyzing a given model, we are not concerned with all possible transitions or traces, but only with those that are actually generated by the model.

**Definition 2 (STG of a model).** Given a model $f = \{f_i\}_{i=1}^n$, we define its STG as

$$ \mathit{STG}_f = \left\{ \langle s, s' \rangle \in \mathbb{B}^n \times \mathbb{B}^n \;\middle|\; \begin{array}{@{}l@{}} \exists i \in \{1, \dots, n\} : s' = s[i \leftarrow f_i(s)], \\ \text{for some } f_i \in f \text{ with } f_i(s) \neq s_i \end{array} \right\} $$

where $s[i \leftarrow v]$ denotes the state obtained from $s$ by replacing the value in component $i$ by value $v$.

Note that when defining the STG of a model, we have forbidden any transition from a state to itself. This is a technical, yet important, detail. The motivation behind this choice is that there is no notion of time when working asynchronously. We are interested in how the system evolves, not in how long it takes to evolve.

As $\mathit{STG}_f$ stores the set of allowed transitions defined by $f$, we can gather the finite traces of the model by computing the least-fixed point of operator $\mathbb{F}_{\mathit{STG}_f}$ over $\wp(\mathcal{T})$ defined by:

$$ \mathbb{F}_{\mathit{STG}_f}(X) = \{ \langle s_0, \dots, s_k, s_{k+1} \rangle \mid \langle s_0, \dots, s_k \rangle \in X \wedge \langle s_k, s_{k+1} \rangle \in \mathit{STG}_f \} $$

when applied to $S_0 := \{\langle s \rangle \mid s \in \mathbb{B}^n\}$. We denote by $\mathcal{T}_f = \mathit{lfp}(\mathbb{F}_{\mathit{STG}_f})(S_0) \subseteq \mathcal{T}$ the set of finite traces of $f$.

## 2.2 Notational Remarks

Throughout the paper, we assume that we are given a model over n variables $f = \{f_i\}_{i=1}^n$ and focus on reducing its dimensionality by removing a given fixed
component $r \in \{1, \dots, n\}$. For presentation purposes, we assume without loss of generality that $r = n$. To that end, the following are ubiquitous.

**Definition 3.** Given a state $s \in \mathbb{B}^n$, we denote by $\bar{s}^i$ the unique state differing from $s$ exactly in the $i$-th component. When $i = n$, we write $\bar{s}$ in place of $\bar{s}^n$. We define the equivalence relationship $\sim$ over $\mathbb{B}^n$ by $s \sim s' \Leftrightarrow s' = \bar{s}$ and denote by $[s] = \{s, \bar{s}\}$ the elements in the equivalence class of $s$. A transition $\langle s, s' \rangle$ is said to be outgoing if $s' \notin [s]$. We denote by $\Delta^n : \mathbb{B}^n \times \mathbb{B}^n \to \{1, \dots, n\}$ the Hamming distance between two states. An STG is said to be well-defined if every transition connects pairs of states at Hamming distance one.

## 2.3 Abstract Interpretation

The main idea behind Abstract Interpretation is to abstract away all parts of a system that are not relevant to the question at hand. This simplification makes it possible to study properties that would otherwise be undecidable or too computationally expensive in the original system. In this paper we rely only on Galois Connection (GC) based Abstract Interpretation. When in the presence of a GC, we have the formal guarantee that the given abstraction is the most precise abstraction that discards the specified information [5].

**Definition 4.** Given $(X, \sqsubseteq)$ and $(Y, \sqsubseteq)$ two partially ordered sets, functions $\alpha : X \to Y$ and $\gamma : Y \to X$ are said to form a Galois Connection if

$$ \forall x \in X, \forall y \in Y : \alpha(x) \sqsubseteq y \Leftrightarrow x \subseteq \gamma(y). \qquad (1) $$

The characteristic condition in (1) is usually denoted by $(X, \sqsubseteq) \stackrel{\gamma}{\underset{\alpha}{\rightleftarrows}} (Y, \sqsubseteq)$.

In Definition 4, set $X$ is called the concrete domain and $Y$ the abstract domain. The function $\alpha$, which takes concrete elements to abstract elements, is called the abstraction function, and the function $\gamma$, which takes abstract elements to concrete elements, is called the concretization function. These functions are said to be adjoints of each other. When there is a GC connection between $X$ and $Y$ for their given partial orders, $\alpha$ uniquely determines $\gamma$ and vice versa. In particular, any function $\beta : X \to Y$ induces a GC, $\langle \wp(X), \sqsubseteq \rangle \stackrel{\beta}{\underset{\alpha}{\rightleftarrows}} \langle \wp(Y), \sqsubseteq \rangle$, from the set of subsets of $X$, and the set of subsets of $Y$, where $\alpha(X) = \{\beta(x) | x \in X\}$ (and $\gamma(Y) = \{x \in X | \beta(x) \in Y\}$). The GCs present in this work are of this form.

In an unusual use of Abstract Interpretation, our concrete and abstract domains are quite similar in nature, differing almost always only in dimensionality. Our concrete objects are the objects in Definition 1. Our abstract objects are the following.

**Definition 5 (Abstract Basic Objects).** An abstract state is an element $s^\# \in \mathbb{B}^{n-1}$. An abstract transition is an ordered pair of abstract states, $\langle x^\#, y^\# \rangle \in \mathbb{B}^{n-1} \times \mathbb{B}^{n-1}$. A finite abstract trace is any k-tuple of abstract states, $\langle s_1^\#, \dots, s_k^\# \rangle \in (\mathbb{B}^{n-1})^k$. An abstract STG is a set of abstract transitions. The set of all $n-1$-dimensional STGs is denoted by $S_{n-1}$. The set of all finite abstract traces is denoted by $T^\# = (\mathbb{B}^{n-1})^*$, the Kleene closure of $\mathbb{B}^{n-1}$. The set of all abstract transitions is denoted by $T_2^\#$, the subset of abstract traces of length two.
To relate our concrete and abstract objects, we introduce abstraction functions over each of these objects that essentially project away the last component in each state making up the object. The point-wise application of these functions gives rise to GCs between their domain and co-domain. When projecting STGs, we choose to exclude all transitions whose projection would look like a transition from a state onto itself. Had we kept these transitions, we would have to exclude them at a later point due to our definitions of STG of a model and well-defined STG. This choice simply relieves us of some extra notation later on.

**Definition 6.** Let $\beta_{\pi_s} : \mathbb{B}^n \to \mathbb{B}^{n-1}$ be the map $s = (s_1, \dots, s_n) \mapsto (s_1, \dots, s_{n-1})$. Similarly, let $\beta_{\pi_T} : \mathcal{T} \to \mathcal{T}^\#$ be the map $\langle s_0, \dots, s_k \rangle \mapsto \langle \beta_{\pi_s}(s_0), \dots, \beta_{\pi_s}(s_k) \rangle$, and let $\beta_{\pi_S} : S_n \to S_{n-1}$ be the map: STG $\mapsto \{\langle x^\#, y^\# \rangle \mid \exists \langle x, y \rangle \in \text{STG} : \langle x^\#, y^\# \rangle = \langle \beta_{\pi_s}(x), \beta_{\pi_s}(y) \rangle \wedge (x^\# \neq y^\#)\}$.

Each of the functions induces a GC, as described before.

# 3 Transition preserving reduction

Here, we propose a simple reduction that preserves all outgoing transitions of the initial model. In doing so, we ensure that any trace in the initial model has a corresponding trace in the reduced model. Conversely, the reduction guarantees that if there is no trace between two states in the reduced model, then there is no trace between either of their counterparts in the initial model.

The first part of this section describes how to obtain the functions of the reduced model functions from those of the initial one. The second part derives the same reduction directly from the model's semantics thanks to Abstract Interpretation. This approach has the advantage of guaranteeing the desired reachability property by construction.

## 3.1 (Syntactic) Reduction Description

Definition 7 explicitly defines a model that preserves all outgoing transitions.

**Definition 7.** Given model $f = \{f_i\}_{i=1}^n$, we define model $\tilde{f} = \{\tilde{f}_i\}_{i=1}^{n-1}$:

$$ \tilde{f}_i(\tilde{s}) = [\tilde{s}_i \Rightarrow (f_i(S^0(\tilde{s})) \wedge f_i(S^1(\tilde{s})))] \wedge [\neg \tilde{s}_i \Rightarrow (f_i(S^0(\tilde{s})) \vee f_i(S^1(\tilde{s})))], $$

where $S^a : \mathbb{B}^{n-1} \to \mathbb{B}^n$ is the map $\tilde{s} \mapsto (\tilde{s}_1, \dots, \tilde{s}_{n-1}, a)$, for $a \in \mathbb{B}$.

Each function in the reduced model $\tilde{f}$ encodes the statement if there is an outgoing transition from the equivalence class, take it. The first condition tracks a change in the updated component's value from 1 to 0 and the second a change from 0 to 1.

The expression above can be simplified by factoring in the effect of the partial assignments on $f_i$ given by $x_n = 0$ and $x_n = 1$ over $f_i(S^0(\tilde{s}))$ and $f_i(S^1(\tilde{s}))$, respectively. This purges any occurrence of the variable $x_n$ from Definition 7.
In Appendix A, we detail how this can be achieved when the functions in $f$ are given in disjunctive normal form (DNF, disjunction of conjunctive clauses). This process shows that the arity of each function may either decrease, if dependencies on some variables become non-functional, or remain unchanged, either due to the introduction of self-regulation or because the function does not depend on the reduced component. However, the computational cost is dominated by formula simplification. In the DNF case, the number of clauses may double. In practice, using Binary Decision Diagrams (BDDs) with maximal sharing yields a more compact normal form and allows for efficient simplification to obtain the reduced functions.

Model $\tilde{f}$ preserves all outgoing transitions defined by $f$ (Theorem 1) and does not introduce new transitions, in the sense that every transition defined by $\tilde{f}$ is necessarily the projection of some transition defined by $f$ (Theorem 2). These two results prove that any trace in the initial model has a corresponding trace in the reduced model and conversely that if there is no trace between two states in the reduced model, then there is no trace between either of their counterparts in the initial model (Lemma 1). The proofs of these results follow immediately from the definition of $\tilde{f}$ and can be found in the Appendix B.

**Theorem 1.** Every outgoing transition in the original model is projected onto the reduced model. $\forall \langle x, y \rangle \in STG_f : (x_n = y_n) \Rightarrow \langle \beta_{\pi_s}(x), \beta_{\pi_s}(y) \rangle \in STG_{\tilde{f}}$.

**Theorem 2.** Every transition in the STG of the reduced model is the projection of an outgoing transition from the original model.

$$ \forall \langle x^{\#}, y^{\#} \rangle \in STG_{\tilde{f}}, \langle S^0(x^{\#}), S^0(y^{\#}) \rangle \in STG_f \text{ or } \langle S^1(x^{\#}), S^1(y^{\#}) \rangle \in STG_f. $$

**Lemma 1.** If there is no trace from state $x^{\#}$ to state $y^{\#}$ in $STG_{\tilde{f}}$, then there is no trace from any $x$ such that $\beta_{\pi_s}(x) = x^{\#}$ to any $y$ such that $\beta_{\pi_s}(y) = y^{\#}$ in $STG_f$. I.e. $x^{\#} \rightsquigarrow y^{\#} \notin STG_{\tilde{f}} \Rightarrow x \rightsquigarrow y \notin STG_f$.

## 3.2 Abstract Interpretation Analysis of the Reduction

In this section, we show how the reduction arises naturally from basic manipulations of the STG of the model. We begin by describing the transformations applied to the STG and demonstrate that the resulting STG satisfies the desired properties. We then outline how the reduced model $\tilde{f}$ can be derived by iteratively abstracting $f$ to reflect these STG-level changes. The goal here is to highlight both the usefulness of reasoning directly with STGs and, more importantly, the mathematical significance of the syntactic transformations in Definition 7. These transformations are not intended for computation, unlike the function simplifications in the syntactic reduction.

To clarify the relationship between original and reduced dynamics, we then define representative reduced traces for each trace of the original model to better understand how each trace is depicted in the reduced model. Finally, we formally establish that the proposed abstraction is the most precise abstraction that preserves all traces while ignoring changes in the reduced component.
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** (a): STG of model *f* = {*f*₁, *f*₂, *f*₃} defined by *f*₁(*s*) = (¬*s*₁ ∧ ¬*s*₃) ∨ (*s*₁ ∧ *s*₂ ∧ ¬*s*₃) ∨ (*x*₁ ∧ *s*₃), *f*₂(*s*) = (¬*s*₃) ∨ (*s*₁ ∧ *s*₃), *f*₃(*s*) = ¬*s*₂. (b): STG obtained by applying *β*<sub>double</sub> to STG*f*. Blue arrows represent added transitions. (c): STG obtained by applying *β*<sub>π<sub>S</sub></sub> ◦ *β*<sub>double</sub> to STG*f*, yielding the reduced STG.</figcaption></figure>

The core idea behind the reduction is to preserve all transitions. This is achieved by duplicating the transitions in the STG to ensure that both states in an equivalence class hold the same information regarding the class’s outgoing transitions. Then, this complemented STG, hereafter referred to as *doubled STG*, is collapsed into a lower-dimensional STG that stores this same information. This process is illustrated in Figure 1.

The first manipulation uses the function $\beta_{\text{double}}$, to give both states of an
equivalence class the same outgoing transitions. In Figure 1 (b), observe that
the sub-STGs defined by $n=0$ and by $n=1$ are split images of each other. As
a result, we can project out the reduced component by $\beta_{\pi_S}$, keeping only one
such sub-STG, which yields the reduced STG in Figure 1 (c).

**Definition 8.** Let $\beta_{\text{double}} : S_n \to S_n$ be such that $\beta_{\text{double}}(\text{STG}) = \{\langle x, y \rangle \mid \langle x, y \rangle \in \text{STG} \lor \langle \bar{x}, \bar{y} \rangle \in \text{STG}\}$.

**Definition 9 (Abstracted STG).** Given a model *f*, we denote by $\text{STG}_f^{\#}$ the STG $\beta_{\pi_S} \circ \beta_{\text{double}}(\text{STG}_f)$, obtained by applying both above manipulations.

Theorem 3 follows immediately by construction. It establishes that $\text{STG}_f^{\#}$ satisfies the desired reachability properties. We emphasize that for results stemming from manipulating STGs, we assume that the starting point is an STG generated by a model (i.e. a well-defined STG) rather than an arbitrary set of transitions. $\text{STG}_f^{\#}$ is thus a well-defined STG itself, and therefore there exists a model that corresponds to it.

We now concern ourselves with establishing that $\text{STG}_f^{\#}$ has the desired prop-
erties. We then find the model defining this STG by successively abstracting the
regulatory functions of the original model and conclude by showing the seman-
tically derived model coincides with the proposed model in Section 3.1.

**Theorem 3.** *Theorems 1 and 2 hold for $\text{STG}_f^{\#}$. That is, every outgoing transition in $\text{STG}_f$ appears as a projected transition in $\text{STG}_f^{\#}$ and every transition in $\text{STG}_f^{\#}$ is necessarily the projection of some outgoing transition in $\text{STG}_f$.*
Towards recovering the model defining $STG_f^\#$, we begin by abstracting the regulatory functions in a way that mimics the effect of $\beta_{\text{double}}$ of doubling the transitions in the STG. This is achieved through the application of the function $\beta_f$.

**Definition 10.** Let $\beta_f : (\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^n \to \mathcal{O}(\mathbb{B}))$ be the function that maps the function $f$ to the abstract function $\beta_f(f)$ collecting both outputs of the input's equivalence class, i.e. $\forall x \in \mathbb{B}^n, \beta_f(f)(x) = \{f(x), f(\bar{x})\}$.

**Definition 11.** We denote by $f^\# = \{\beta_f(f_i)\}_{i=1}^n$ the result of applying the abstraction function $\beta_f$ to each regulatory function in the model $f$, and define its STG as:

$$STG_{f^\#} = \left\{ \langle s, s' \rangle \in \mathbb{B}^n \times \mathbb{B}^n \;\middle|\; \begin{array}{l} \exists i \in \{1, \dots, n\} : s' = s[i \leftarrow b], \\ \text{where } b \in \beta_f(f_i)(s) \text{ for some } f_i \in f^\# \text{ and } b \neq s_i \end{array} \right\}.$$

We call attention to the fact that $STG_f^\#$ is the STG obtained by applying the transformation $\beta_{\pi_S} \circ \beta_{\text{double}}$ to $STG_f$, whereas $STG_{f^\#}$ is the STG defined by the tentative abstract model $f^\#$ obtained by abstracting the regulatory functions in $f$. These two STGs in no way coincide. That being said, $STG_{f^\#}$ coincides with $\beta_{\text{double}}(STG_f)$, by construction, as stated by Lemma 2.

**Lemma 2.** $\beta_{\text{double}}(STG_f) \equiv STG_{f^\#}$.

Now, to mimic the effect of $\beta_{\pi_S}$, we need to decrease the dimensionality of the abstracted functions. As we are preserving all outgoing transitions from an equivalence class, we keep the output value disagreeing with the current value of the component $i$ if it exists. Formally, we achieve this through the following collapsing functions:

**Definition 12.** For each $i < n$, let $\beta_{\text{collapse}}^i : (\mathbb{B}^n \to \mathcal{O}(\mathbb{B})) \to (\mathbb{B}^{n-1} \to \mathbb{B})$ be the function taking an abstract function $f$ over $n$ variables and mapping it to the concrete function $\beta_{\text{collapse}}^i(f)$ over $n-1$ variables by

$$\beta_{\text{collapse}}^i(f)(\tilde{s}) = \begin{cases} 1 - \tilde{s}_i, & \text{if } 1 - \tilde{s}_i \in f(s) \text{ for some } s \text{ such that } \tilde{s} = \beta_{\pi_S}(s) \\ \tilde{s}_i, & \text{else.} \end{cases}$$

**Definition 13 (Abstracted Model).** We denote by $\tilde{f}' = \langle \beta_{\text{collapse}}^i \circ \beta_f(f_i) \rangle_{i=1}^{n-1}$ the model obtained by means of consecutively applying abstractions $\beta_{\text{collapse}}^i$ and $\beta_f$ to the functions in model $f$. We denote its STG by $STG_{\tilde{f}}$.

Not only does $STG_{\tilde{f}}$, coincide with the abstracted $STG_f^\#$ (Lemma 3), but model $\tilde{f}'$ itself also matches the syntactically defined model $\tilde{f}$ given in Definition 7 (Theorem 4).

**Lemma 3.** $STG_f^\# \equiv STG_{\tilde{f}}$.
**Theorem 4.** The abstracted model $\tilde{f}'$ coincides with the syntactically proposed model $\tilde{f}$ in Definition 7.

We have shown that all transitions in the original model are preserved by the reduction. In the same way, every trace in the original model is mapped to a corresponding trace in the reduced model. Yet, the converse does not hold. Effectively, the reduction introduces fictitious transitions and thus fictitious traces (see panels (a) and (e) in Figure 4). This is the inherent trade-off for preserving transition model reductions. Indeed, at this level of abstraction, we ignore the difference between two equivalent states (which are equal except on the n-th component), which allows forming traces by chaining transitions that spontaneously flip, in their states, the value of the n-th component.

Lemma 4 capitalizes on the fact that all transitions are preserved to show that every trace in the original model $f$ has a corresponding trace in the reduced model $\tilde{f}$. This corresponding reduced trace suppresses transitions in the reduced component by applying the function $\beta_{\text{rdup}}$, as these transitions cannot be observed in the reduced model.

**Definition 14.** Let $\beta_{\text{rdup}} : \mathcal{T}^{\#} \to \mathcal{T}^{\#}$ be the function that removes all consecutive duplicates of a state.

**Lemma 4.** $\forall t \in \mathcal{T}_f : \beta_{\text{rdup}} \circ \beta_{\pi_T}(t) = t^{\#} \in \mathcal{T}_{\tilde{f}}$.

We say $t^{\#} = \beta_{\text{rdup}} \circ \beta_{\pi_T}(t)$ is the representative of $t$. In fact, we have a partition of $\mathcal{T}$ under the image of $\beta_{\text{rdup}} \circ \beta_{\pi_T}$.

**Lemma 5.** The function $\beta_{\text{rdup}} \circ \beta_{\pi_T}$ induces an equivalence relationship over $\mathcal{T}$ by:

$$t \sim t' \Leftrightarrow \beta_{\text{rdup}} \circ \beta_{\pi_T}(t) = \beta_{\text{rdup}} \circ \beta_{\pi_T}(t').$$

Two traces $t$ and $t'$ are in the same equivalence class if they have the same representative trace. We denote by $[x]_{\sim}$ the elements in the equivalence class of trace $x$ i.e. $[x]_{\sim} = \{y \in \mathcal{T} \mid \beta_{\text{rdup}}(\beta_{\pi_T}(x)) = \beta_{\text{rdup}} \circ \beta_{\pi_T}(y)\}$ and by $[X]_{\sim} = \cup_{x \in X}[x]_{\sim}$ the elements in the equivalence class of some trace $x \in X$.

This partition begs the question: *exactly which traces get mapped to the same trace?* Towards answering this question better, we introduce the two following upper-closure operators.

**Definition 15.** Let $\rho_{\pi} : \wp(\mathcal{T}) \to \wp(\mathcal{T})$ be the upper-closure operator that takes a set of traces and returns all the traces with the same image under $\beta_{\pi_T}$, i.e.

$$\rho_{\pi}(X) = \{t \in \mathcal{T} \mid \exists x \in X : \beta_{\pi_T}(t) = \beta_{\pi_T}(x)\}.$$

**Definition 16.** Let $\rho_{\text{osci}} : \wp(\mathcal{T}) \to \wp(\mathcal{T})$ be the upper-closure operator that takes a set of traces and returns all traces with the same image under $\beta_{\text{osci}}$, i.e.

$$\rho_{\text{osci}}(X) = \{t \in \mathcal{T} \mid \exists x \in X : \beta_{\text{osci}}(t) = \beta_{\text{osci}}(x)\},$$

where $\beta_{\text{osci}} : \mathcal{T} \to \mathcal{T}$ is the function that compresses consecutive states in a same equivalence class to the first appearing state in this equivalence class.
<figure><img src="image_3.png" /><figcaption>Fig. 2. Operators $\rho_{\text{osci}}$ and $\rho_{\pi}$.</figcaption></figure>

Closing a trace under these operators coincides with gathering the elements in its equivalence class as defined by $\beta_{\text{rdup}} \circ \beta_{\pi_T}$. This result implies that the operators $\rho_{\text{osci}}$ and $\rho_{\pi}$ commute.

**Theorem 5.** $\forall X \in \wp(\mathcal{T})$, $\rho_{\pi} \circ \rho_{\text{osci}}(X) = \rho_{\text{osci}} \circ \rho_{\pi}(X) = [X]_{\sim}$.

Theorem 5 is illustrated in Figure 2. It tells us that traces entering the same equivalence classes in the same order are mapped to the same representative trace. Thus, the reduction is not sensitive to where in the equivalence class the system is and to how long it may remain in it.

As our upper-closure operators commute, by Ore's Theorem [20], we get that their composition is also an upper-closure operator. In terms of Abstract Interpretation, the fact that they commute guarantees that our abstraction is the most precise abstraction reducing the given component while preserving all outgoing transitions [28], which gives us the GC in Theorem 6.

**Theorem 6.** The function $\beta_{\text{rdup}} \circ \beta_{\pi_T}$ induces $(\wp(\mathcal{T}), \subseteq) \xleftarrow{\gamma_{\text{Reach}}} (\wp(\mathcal{T}^{#}), \subseteq)$.

Even if the reduction introduces spurious traces, the GC in Theorem 6 guarantees that the proposed reduced model introduces the fewest possible superfluous traces necessary while preserving all true traces when removing the specified component. That is, among all possible reductions that project away this component while capturing all traces of the initial model, our reduced model most closely approximates the behavior of the original model.

# 4 Naldi et al.'s Reduction Revisited

In this section, we formalize the well-known Naldi et al.'s reduction [15,16] using Abstract Interpretation to clarify which behaviors of the original model are preserved and discarded. As a by-product of this analysis, we obtain a natural generalization that extends the applicability of the original method.

Naldi et al.'s reduction [15,16] is based on the idea that if a component evolves significantly faster than the remaining, its evolution can be made implicit. This is motivated by the fact that biological processes take place in vastly different time-scales. The reduction preserves stable states and cyclical attractors, ensures that connected components in the reduced model come from connected components in the original model, and ensures that complex attractors in the reduced model
come from at most one complex attractor in the original (see panels (a) and (b) in Figure 4). As such, it remains the standard reduction for BNs.

However, the reduction achieves this dynamical consistency by requiring the reduced component to be non-self-regulated and by selectively discarding some transitions defined by the original model in the reduction process. This process makes it unsuitable to address the same type of questions as the reduction introduced in Section 3 is designed to.

Using a bottom-up approach, we formalize the effect of prioritizing the updates of the reduced component over the updates of the remaining. We start from the STG of the model and work our way up to traces without imposing any conditions on the reduced component. We then establish that when a component is not self-regulated, our abstraction recovers the same behavior as Naldi et al.'s reduction.

## 4.1 STG transformations

This section describes the basic operations performed over the STG of a model leading to a smaller STG encoding exclusively the original traces of the model respecting the given time-scale separation. Once again, we are not interested in the effective computation of the semantic transformations of the reduction, which we know exists because the resulting STG is well-defined (e.g. see Definition 3) and thus corresponds to a model, but rather on its semantical foundations.

Our first step is to modify the transitions of the STG so that they comply with the priority allocated to the evolution of the reduced component. The key idea is that we can effectively fuse together a transition relating to this component with all possible next transitions.

**Definition 17.** Let $\beta_{\text{valid}}: S_n \to S_n$ be the map $STG \mapsto STG^\subseteq \cup STG^{\Delta^2}$ where

$$STG^\subseteq = \{\langle s, s' \rangle \in STG \mid (s' \neq \bar{s}) \wedge (\langle \bar{s}, s \rangle \in STG \vee (\langle s, \bar{s} \rangle, \langle \bar{s}, s \rangle \notin STG))\}$$

is the subset containing only outgoing transitions from states that are either the target of a transition in the reduced component or such that their equivalence class contains no transitions and where

$$STG^{\Delta^2} = \{\langle s, s' \rangle \in \mathbb{B}^n \times \mathbb{B}^n \mid (s \neq s') \wedge \langle s, \bar{s} \rangle \in STG \wedge \langle \bar{s}, s' \rangle \in STG\}$$

is the set of transitions obtained by fusing together a (fast) transition in the reduced component with a subsequent transition from its target state.

Function $\beta_{\text{valid}}$ transforms an STG into a valid STG under the fixed time-scale separation (which may, it this intermediary reduction step include some transitions between states at Hamming distance 2). This process is illustrated in Figure 3. Once in the presence of a valid STG, we once again proceed by reducing its dimensionality by means of $\beta_{\pi_S}$. By construction, the resulting STG faithfully encodes all valid traces. This faithfulness is formalized by GC in Theorem 7 and detailed in Section 4.2. The same GC holds when restricted to only well-defined STGs in both dimensions.
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** (a): STG of model $f = \{f_1, f_2, f_3\}$ defined by $f_1(s) = (\neg s_1 \land \neg s_3) \lor (s_1 \land s_2 \land \neg s_3) \lor (x_1 \land s_3)$, $f_2(s) = (\neg s_3) \lor (s_1 \land s_3)$, $f_3(s) = \neg s_2$. (b): STG obtained from applying $\beta_{\text{valid}}$ to STG$_f$, where dashed arrows represent removed transitions and blue arrows represent added (fused) transitions. (c): STG obtained by applying $\beta_{\pi_S} \circ \beta_{\text{valid}}$ to STG$_f$, yielding the reduced STG.</figcaption></figure>

**Theorem 7.** Function $\beta_{\pi_S} \circ \beta_{\text{valid}}$ induces $\langle \wp(S_n), \subseteq \rangle \xleftarrow{\gamma_{\text{Naldi}}} \langle \wp(S_{n-1}), \subseteq \rangle$.

We use $\alpha_{\text{Naldi}}$ and $\gamma_{\text{Naldi}}$ to highlight that when the reduced component satisfies Naldi et al.'s conditions, our semantic transformations precisely match the effect of the reduction, effectively resulting in the same reduced model. Subsection 4.3 outlines how to establish this result.

## 4.2 Valid Traces and Preserved Traces

In this section we demonstrate how we can extract and encode the desired set of traces (i.e. the ones respecting the time-scale separation principle) from STG manipulations described in the previous section. We first make precise what it means for a trace defined by model $f$ to be valid under the specified time-scale separation principle.

**Definition 18.** We denote by $V_f$ the valid traces of $f$, i.e. the set of traces that comply with the specified time-scale separation while avoiding oscillatory<fnref n="3" /> behaviors, where:

$$ V_f = \{T \in \mathcal{T}_f | \forall \langle s_i, s_{i+1} \rangle \in T: (s_{i+1} = \bar{s}_i) \Rightarrow (s_{i+2} \neq s_i) \land \\ \land (s_{i+1} \neq \bar{s}_i) \Rightarrow (\forall T' \in \mathcal{T}_f : \langle s_i, \bar{s}_i \rangle \notin T' \lor \exists T' \in \mathcal{T}_f : \langle \bar{s}_i, s_i \rangle \in T')\}. $$

In words, at any given state if we move towards the other state in the equivalence class, the next transition must be an outgoing transition and if we move outside the equivalence class, it is either because there is no (fast) transition

<footnote n="3">³ Strictly speaking, as transitions updating the reduced component are to be prioritized, negative self-regulations induce oscillations within an equivalence class. These oscillations are unobservable when the component is projected out. Moreover, it is also reasonable to assume that if there is a transition that breaks this cycle, the system should eventually take it. Thus we allow for controlled violations of the time-scale separation principle by altogether avoiding these oscillations, which are both presumably escapable and unobservable.</footnote>
updating the removed component or because we are already the target of such a (fast) transition.

We now prove that the set of valid traces of a model is generated by the resulting STG from our first STG manipulation. But first, as we broke the asynchronicity of the STG of $f$ by applying $\beta_{valid}$, we need to define a function that interprets the fused transitions appearing in a trace as a composition of their correct asynchronous counterparts.

**Definition 19.** We denote by $\gamma_{2-to-1}: \wp(T) \to \wp(T)$ the function that takes a set of traces and maps each trace $t$ in it to trace $t'$ obtained by replacing each occurrence of $\langle s, s' \rangle$ such that $\Delta^n(\langle s, s' \rangle) = 2$ by $\langle s, s'', s' \rangle$ where $s'' = \bar{s}$.

Note that when starting from an arbitrary STG rather than from a well-defined STG generated by a model, this translating function would not be able to correctly recover the two transitions that fused together, thus we emphasize the subscript $f$ in the following results. Theorem 8 tells us the valid traces of $f$ are the "translated" traces of $\beta_{valid}(STG_f)$. That is, $\beta_{valid}(STG_f)$ encodes exactly all valid traces of $f$. Recall that operator $\mathbb{F}$ simply extends traces by all possible next transitions according to a given STG.

**Theorem 8.** $V_f = \gamma_{2-to-1}(\mathbf{lfp}(\mathbb{F}_{\beta_{valid}(STG_f)})(\tilde{S}_0))$.

The next theorem establishes that all traces in $V_f$ have a corresponding trace in the projected STG. We say corresponding because the reduced model is blind to any transition in the reduced component. To cope with this we employ $\beta_{rdup}$ once again.

**Theorem 9.** Letting $\tilde{S}_0 = \{\langle \tilde{s} \rangle | s \in \tilde{\mathbb{B}}^{n-1}\}$, we have

$$ \mathbf{lfp}(\mathbb{F}_{\beta_{\pi_S} \circ \beta_{valid}(STG_f)})(\tilde{S}_0) = \beta_{rdup} \circ \beta_{\pi_T}(V_f). $$

Theorem 9 states that the abstracted STG, $\beta_{\pi_S} \circ \beta_{valid}(STG)$ stores all valid traces of $f$, once interpreted. It remains to explicitly recover the model defining this STG. The next section relates the traces of the abstracted STG to those of Naldi et al.'s reduced model. We prove that when the reduced component is not self-regulated, we recover the STG defined by Naldi et al.'s reduced model, thus effectively proving that Naldi et al.'s reduction appears as a special case of the proposed semantic abstraction where no impositions were made on the reduced component.

## 4.3 Naldi et al.'s reduction matches the proposed abstraction

We adopt the following notions from Naldi et al.

**Definition 20.** Given a component $i$, if $f_i$ is independent of $s_i$, i.e. if $\forall s \in \mathbb{B}^n$, $f_i(s) = f_i(\bar{s}^i)$, we say $i$ is reducible. When $i$ is reducible, we denote by $\mathcal{R}^i(s)$ the unique state in equivalence class $\{s, \bar{s}^i\}$ such that $f_i(s) = s_i$. We call this state the representative state of the equivalence class. When clear from context, we may also use $\mathcal{R}^i(\tilde{s})$ to denote this same state, where $\tilde{s}$ is the image of $s$ when component $i$ is projected away.
If component *n* is not self-regulated, then *f*<sub>*n*</sub> is reducible. As a consequence, there is exactly one transition of the form ⟨s, s̄⟩ in every equivalence and thus every class has a unique representative state. This assumption makes it so that the first condition in Definition 18 is always satisfied and that the second condition can be simplified to (*s*<sub>*i*+1</sub> ≠ s̄<sub>*i*</sub>) ⇒ ⟨*s*<sub>*i*</sub>, s̄<sub>*i*</sub>⟩ ∉ STG<sub>*f*</sub>. Similarly, applying β<sub>valid</sub> to STG<sub>*f*</sub> amounts to first purging all transitions updating the reduced component and all outgoing transitions from the non-representative states in each equivalence class, and then adding the necessary fused transitions from non-representative states to successor states of their representatives.

With these simplifications, the proof of Theorem 10 becomes quite straight-
forward. This result establishes that Naldi et al.'s reduction generates the same
traces as the ones defined by the STG of our abstraction, thus effectively proving
that both processes defined the same model as hinted at before.

**Theorem 10.** For any given model, *f* = {*f*<sub>*i*</sub>}<sub>*i*=1</sub><sup>*n*</sup> such that *n* is reducible, letting
*f̃* = {*f̃*<sub>*i*</sub>}<sub>*i*=1</sub><sup>*n*−1</sup> denote the reduced model obtained by Naldi et. al.'s reduction, we
have that **lfp**(<span style="text-decoration: overline;">F</span><sub>β<sub>π<sub>S</sub></sub> ◦ β<sub>valid</sub>(STG<sub>*f*</sub>)</span>)(*S̃*<sub>0</sub>) = *T*<sub>*f*</sub>.

**5 Conclusion and Discussion**

In this work, we introduced and studied the semantics of two complementary re-
duction techniques for Boolean Networks, a new transition-preserving reduction
and a generalized version of Naldi et. al.'s reduction. Both aim at simplifying
models by removing a given component, but are designed to preserve different
properties, namely reachability and dynamical consistency, respectively.

The transition-preserving reduction is designed to maintain all transitions of the original model after removing a component. As a result, every trace in the original model has a corresponding trace in the reduced model. This makes the reduction sound for reasoning about non-reachability. Non-reachability in the reduced model implies non-reachability in the original (see panels (a) and (c) in Figure 4).

This guarantee comes at a cost. The reduced model may include spurious
traces that do not correspond to any behavior in the original model. Conse-
quently, some dynamical properties, such as attractors or stable states, may
be lost or altered (see panels (a) and (e)). It is important not to interpret the
transition-preserving reduced model as a compactification of the original model.
In fact, the syntactic structure, including the regulatory graph, may change sub-
stantially. This is evidenced by the introduction of self-regulations (see panels
(a), (c), and (e)) on non-reduced components.

Nonetheless, the transition-preserving reduction is minimal in the number of
spurious traces it introduces, in the sense that among all reductions eliminating
the same component and preserving all transitions, it introduces the fewest pos-
sible spurious traces. This result is formally guaranteed thanks to the use of best
abstraction functions, as usually done in the Abstract Interpretation framework.

This approach of reasoning about the STG itself also suggests a possible
strategy to choose which component to reduce. In principle, one could select
a component whose abstraction introduces the fewest spurious behaviors. In this context, it may be worth investigating the role of negatively self-regulated components, particularly those giving rise to the most functional loops within their equivalence classes.

The second part of the paper focused on reinterpreting the well-known reduction by Naldi et al. based on a time-scale separation principle. This reinterpretation clarifies both the rationale behind the reduction and its limitations. In fact, by analyzing the semantic foundations of Naldi et al.'s reduction, we formalized precisely which behaviors of the initial model are preserved by the reduction, and extended its applicability to any node in the model, not just the non-self-regulated nodes allowed by the original reduction.

While we showed that Naldi et al.'s reduction emerges as a special case of this semantic analysis, we did not explicitly (syntactically) recover the model defining the reduced STG in the general case, nor did we analyze which properties are preserved when the requirement that the reduced component must not be self-regulated is relaxed. Despite this lose end, we know that this syntactic recovery is possible because the reduced STG corresponds to the STG defined by a model by construction. Regarding the dynamical implications of reducing an arbitrary node, we expect that stable states and attractors arising from positive self-regulated components may be lost or modified (see panels (a) and (d)).

Recent work by Schwieger and Tonello [22] extends the attractor-preserving reduction to negatively self-regulated components. Our abstraction should naturally encompass this extension as well. Proving this formally, however, would require introducing the notion of *fairness*, to properly justify preserving all outgoing transitions from states involved in oscillations induced by negative self-regulations. This lies beyond the scope of this work as fairness requires reasoning over infinite traces.

Finally, both reduction methods can be applied iteratively. The original Naldi et. al.'s reduction is known to be order sensitive. That is, the applicability of reductions may depend on the order in which components are removed: a given order may give rise to a self-regulation, thus blocking further reduction, and another order may deem certain self-regulations non-functional, thus allowing for further reduction. In contrast, both the generalized abstraction and the transition-preserving reduction do not suffer from this limitation.

Although this work has focused on theoretical foundations, we plan to implement the transition-preserving reduction in BioLQM, making it accessible via GINsim and the CoLoMoTo notebook. This implementation should be straightforward, as the reduced model is explicitly defined. Extending these reduction methods to multi-valued models would be a natural next step. Abstract interpretation provides a promising theoretical framework to support this extension.

**Acknowledgments.** This project has received funding from the European Union's MSCA-Horizon Europe, grant agreement No 101126554. Views and opinions expressed are however those of the author(s) only and do not neces-
<figure><img src="image_5.png" /><figcaption>**Fig. 4.** Reduction methods illustrated: regulatory graphs on the left (green arrows for activations, red hammered edges for inhibitions, blue for dual interactions), their STGs on the right, preservability, loss or appearance of attractors and specific traces indicated for each model version, asterisks in states denote reduced variables.</figcaption></figure>
sarily reflect those of the European Union. Neither the European Union nor the
granting authority can be held responsible for them.

References

1. Abou-Jaoudé, W., Feret, J., Thieffry, D.: Derivation of qualitative dynamical models from biochemical networks. In: Roux, O.F., Bourdon, J. (eds.) Computational Methods in Systems Biology - 13th International Conference, CMSB 2015, Nantes, France, September 16-18, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9308, pp. 195-207. Springer (2015). https://doi.org/10.1007/978-3-319-23401-4_17

2. Abou-Jaoudé, W., Thieffry, D., Feret, J.: Formal derivation of qualitative dynamical models from biochemical networks. Biosystems **149**, 70–112 (2016). https://doi.org/10.1016/j.biosystems.2016.09.001

3. Abou-Jaoudé, W., Traynard, P., Monteiro, P.T., Saez-Rodriguez, J., Helikar, T., Thieffry, D., Chaouiya, C.: Logical modeling and dynamical analysis of cellular networks. Frontiers in Genetics **7** (2016). https://doi.org/10.3389/fgene.2016.00094

4. Beica, A., Feret, J., Petrov, T.: Tropical abstraction of biochemical reaction networks with guarantees. In: Gupta, A., Petrov, T. (eds.) Proceedings of SASB 2018, the Ninth International Workshop on Static Analysis and Systems Biology, Freiburg, Germany - August 28th, 2018. Electronic Notes in Theoretical Computer Science, vol. 350, pp. 3–32. Elsevier (2020). https://doi.org/10.1016/J.ENTCS.2020.06.002

5. Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)

6. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 238-252. ACM Press, New York, NY, Los Angeles, California (1977)

7. Fages, F., Soliman, S.: Abstract interpretation and types for systems biology. Theor. Comput. Sci. **403**(1), 52-70 (2008). https://doi.org/10.1016/J.TCS.2008.04.024

8. Feret, J.: Model reduction of infinite rule-based models. In: Uhrmacher, A. (ed.) Conference Record of the thirty-ninth Annual ACM SIGSIM International Conference on Principles of Advanced Discrete Simulation. ACM Press, New York (2025). https://doi.org/10.1145/3726301.3728414, to appear

9. Feret, J., Danos, V., Krivine, J., Harmer, R., Fontana, W.: Internal coarse-graining of molecular systems. Proceedings of the National Academy of Sciences **106**(16), 6453-6458 (2009). https://doi.org/10.1073/pnas.0809908106

10. Feret, J., Koepp, H., Petrov, T.: Stochastic fragments: A framework for the exact reduction of the stochastic semantics of rule-based models. Int. J. Softw. Informatics **7**(4), 527-604 (2013), http://www.ijsi.org/ch/reader/view禄 ABSTRACT. aspx?file_no=i173

11. Feret, J., Salazar, A.: A generic framework to coarse-grain stochastic reaction networks by abstract interpretation. In: Dragoi, C., Emmi, M., Wang, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 24th International
Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13881, pp. 228-251. Springer (2023). https://doi.org/10.1007/978-3-031-24950-1_11, https://doi.org/10.1007/978-3-031-24950-1_11

12. Folschette, M., Paulevé, L., Magnin, M., Roux, O.F.: Sufficient conditions for reachability in automata networks with priorities. Theor. Comput. Sci. **608**, 66-83 (2015). https://doi.org/10.1016/J.TCS.2015.08.040, https://doi.org/10.1016/j.tcs.2015.08.040

13. Grieco, L., Calzone, L., Bernard-Pierrot, I., Radvanyi, F., Kahn-Perlès, B., Thieffry, D.: Integrative modelling of the influence of mapk network on cancer cell fate decision. PLoS Computational Biology **9**(10), e1003286 (Oct 2013). https://doi.org/10.1371/journal.pcbi.1003286

14. Kauffman, S.A.: Metabolic stability and epigenesis in randomly constructed genetic nets. J. Theor. Biol. **22**(3), 437-467 (1969)

15. Naldi, A., Remy, E., Thieffry, D., Chaouiya, C.: A reduction of logical regulatory graphs preserving essential dynamical properties. In: Computational Methods in Systems Biology: 7th International Conference, CMSB 2009 Proceedings. pp. 266-280. Springer (2009)

16. Naldi, A., Remy, E., Thieffry, D., Chaouiya, C.: Dynamically consistent reduction of logical regulatory graphs. Theoretical Computer Science **412**(21), 2207-2218 (2011)

17. Naldi, A.: Biolqm: A java toolkit for the manipulation and conversion of logical qualitative models of biological networks. Frontiers in Physiology **9** (Nov 2018). https://doi.org/10.3389/fphys.2018.01605

18. Naldi, A., Hernandez, C., Abou-Jaoudé, W., Monteiro, P.T., Chaouiya, C., Thieffry, D.: Logical modeling and analysis of cellular regulatory networks with ginsim 3.0. Frontiers in Physiology **9** (Jun 2018). https://doi.org/10.3389/fphys.2018.00646

19. Naldi, A., Hernandez, C., Levy, N., Stoll, G., Monteiro, P.T., Chaouiya, C., Helikar, T., Zinovyev, A., Calzone, L., Cohen-Boulakia, S., Thieffry, D., Paulevé, L.: The colomoto interactive notebook: Accessible and reproducible computational analyses for qualitative biological networks. Frontiers in Physiology **9** (Jun 2018). https://doi.org/10.3389/fphys.2018.00680

20. Ore, O.: Combinations of closure relations. The Annals of Mathematics **44**(3), 514 (Jul 1943). https://doi.org/10.2307/1968978

21. Paulevé, L., Magnin, M., Roux, O.F.: Static analysis of biological regulatory networks dynamics using abstract interpretation. Math. Struct. Comput. Sci. **22**(4), 651-685 (2012). https://doi.org/10.1017/S0960129511000739, https://doi.org/10.1017/S0960129511000739

22. Schwieger, R., Tonello, E.: Reduction for asynchronous boolean networks: elimination of negatively autoregulated components. Discrete Mathematics & Theoretical Computer Science **25**(Automata, Logic and Semantics) (2024)

23. Sugita, M.: Functional analysis of chemical systems in vivo using a logical circuit equivalent. ii. the idea of a molecular automaton. J. Theor. Biol. **4**(2), 179-192 (1963). https://doi.org/10.1016/0022-5193(63)90027-4

24. Thomas, R.: Boolean formalization of genetic control circuits. J. Theor. Biol. **42**(3), 563-585 (1973)

25. Thomas, R.: Regulatory networks seen as asynchronous automata: A logical description. J. Theor. Biol. **153**, 1-23 (1991)
26. Thomas, R., d'Ari, R.: Biological Feedback. CRC Press, Inc. (1990), https://hal.science/hal-00087681v1/, 316 page book published in 1990. Online version available.

27. Wang, R.S., Saadatpour, A., Albert, R.: Boolean modeling in systems biology: an overview of methodology and applications. Phys Biol. 9(5), 055001 (2012). https://doi.org/10.1088/1478-3975/9/5/055001

28. Ward, M.: The closure operators of a lattice. The Annals of Mathematics 43(2), 191 (Apr 1942). https://doi.org/10.2307/1968865
## A General Remarks

As mentioned at the very end of Section 2, each $\beta$ function defines a GC between their respective concrete and abstract objects. We include these results here to introduce the necessary $\gamma$ and $\alpha$ functions to follow the subsequent proofs.

**Lemma 6.** $(\wp(\mathbb{B}^n), \subseteq) \underset{\alpha_s}{\overset{\gamma_s}{\rightleftarrows}} (\wp(\mathbb{B}^{n-1}), \subseteq)$ where $\alpha_s(X) = \{\beta_{\pi_s}(x) | x \in X\}$ and $\gamma_s(Y) = \{x \in \wp(\mathbb{B}^n) | \exists y \in Y : \beta_{\pi_s}(x) = y\}$.

**Lemma 7.** $(\wp(T), \subseteq) \underset{\alpha_T}{\overset{\gamma_T}{\rightleftarrows}} (\wp(T^#), \subseteq)$ where $\alpha_T(X) = \{\beta_{\pi_T}(x) | x \in X\}$ and $\gamma_T(Y) = \{x \in T | \exists y \in Y : \beta_{\pi_T}(x) = y\}$.

**Lemma 8.** $(\wp(S_n), \subseteq) \underset{\alpha_S}{\overset{\gamma_S}{\rightleftarrows}} (\wp(S_{n-1}), \subseteq)$ where $\alpha_S(X) = \{\beta_{\pi_S}(x) | x \in X\}$ and $\gamma_S(Y) = \{x \in \wp(S_n) | \exists y \in Y : \beta_{\pi_S}(x) = y\}$.

### A.1 On simplifying the reduced model in Section 3

As promised, this section describes how to simplify the reduced model when the original model is in Disjunctive Normal Form (DNF).

Without loss of generality, we assume that $r = n$ to avoid index mismatching for presentation purposes. If each $f_i \in f$ is given in DNF, i.e. $f_i = \bigvee_{j=1}^{n_i} C_j^i$, we can split its clauses depending on whether they depend on the value of the removed component or not:

$$C_i^{\perp} = \{C_j^i \in f_i | s_n \notin C_j^i \wedge \neg s_n \notin C_j^i\} \text{ and } C_i^{\parallel} = \{C_j^i \in f_i | s_n \in C_j^i \vee \neg s_n \in C_j^i\}.$$

As $s_n$ and $\neg s_n$ cannot appear together in the same clause, we may further split $C^{\perp}$ into clauses with $s_n$ and clauses containing $\neg s_n$:

$$^{+}C_i^{\perp} = \{C_j^i \in C_i^{\perp} | s_n \in C_j^i\} \text{ and } ^{-}C_i^{\perp} = \{C_j^i \in C_i^{\perp} | \neg s_n \in C_j^i\}.$$

From Definition 7, $f_i(S^0(\tilde{s}))$ and $f_i(S^1(\tilde{s}))$ now become:

$$ \begin{aligned} f_i(S^0(\tilde{s})) &= \bigvee_{C \in C_i^{\perp}} (C \setminus \{\neg s_n\}) \vee \bigvee_{C \in C_i^{\perp}} C \\ f_i(S^1(\tilde{s})) &= \bigvee_{C \in C_i^{\parallel}} (C \setminus \{s_n\}) \vee \bigvee_{C \in C_i^{\parallel}} C. \end{aligned} $$

Replacing $f_i(S^0(\tilde{s}))$ and $f_i(S^1(\tilde{s}))$ in Definition 7 by the above expressions and simplifying until we reach a DNF yields:

$$ \begin{aligned} \tilde{f}_i(s) &= \bigvee_{C \in C_i^{\perp}} C \vee \bigvee_{C \in C_i^{\perp}} [(C \setminus \{\neg s_n\}) \cup \{\neg s_i\}] \vee \\ & \quad \bigvee_{C \in C_i^{\parallel}} [(C \setminus \{s_n\}) \cup \{\neg s_i\}] \vee \\ & \quad \bigvee_{C \in C_i^{\parallel}} [(C^+ \setminus \{s_n\}) \cup (C^- \setminus \{\neg s_n\})]. \end{aligned} \quad (2) $$
Arguably, the presentation given in Definition 7 is far more compact, even with implementation purposes in mind. Of course, many of these modified conjunctions are prone to being falsified, which would heavily relieve the number of terms in $\tilde{f}_i$. Regardless, this endeavor has been fruitful, for it evidences how the reduced model may induce negative self-regulations on the remaining components, or override existing positive self-regulations.

## B Proof Appendix for Section 3

Again, we assume the reduced component to be the last component to avoid index mismatching.

*Proof (of Theorem 1).* Let $\langle x, y \rangle$ be an outgoing transition in $SGT_f$. Then by definition $\exists i < n$ such that $y_i = f_i(x) \neq x_i$. Let $x^\# = \beta_{\pi_s}(x)$ and $y^\# = \beta_{\pi_s}(y)$.

If $x_i = 0$, then $f_i(x) = 1$ and at least one, $S^0(x^\#)$ or $S^1(x^\#)$, is such that $f_i(S^0(x^\#)) = 1$ or $f_i(S^1(x^\#)) = 1$. By definition of $\tilde{f}_i(x^\#)$, both implications evaluate to true, and thus $\tilde{f}_i(x^\#) = 1$, meaning $\langle x^\#, y^\# \rangle \in STG_{\tilde{f}}$, as desired.

If $x_i = 1$, then $f_i(x) = 0$ and at least one, $S^0(x^\#)$ or $S^1(x^\#)$, is such that $f_i(S^0(x^\#)) = 0$ or $f_i(S^1(x^\#)) = 0$. By definition of $\tilde{f}_i(x^\#)$, the first implication evaluates to false, thus making $\tilde{f}_i(x^\#) = 0$ and $\langle x^\#, y^\# \rangle \in STG_{\tilde{f}}$ again. ■

*Proof (of Theorem 2).* Consider a transition $\langle x^\#, y^\# \rangle \in STG_{\tilde{f}}$. Then $\exists i < n$: $y_i^\# = \tilde{f}_i(x^\#) \neq x_i^\#$.

If $x_i^\# = 0$ then $\tilde{f}_i(x^\#) = 1$. By definition of $\tilde{f}_i(x^\#)$, both implications must evaluate to true and thus $f_i(S^0(x^\#)) \lor f_i(S^1(x^\#))$ evaluates to true, meaning either $\langle S^0(x^\#), S^0(y^\#) \rangle$ or $\langle S^1(x^\#), S^1(y^\#) \rangle$ is in $STG_f$.

If $x_i^\# = 1$ then $\tilde{f}_i(x^\#) = 0$. By definition of $\tilde{f}_i(x^\#)$, as the second implication in $\tilde{f}_i(x^\#)$ is necessarily true, the first must be false, implying $f_i(S^0(x^\#)) \land f_i(S^1(x^\#)) = 0$ and thus at least one $\langle S^0(x^\#), S^0(y^\#) \rangle$ or $\langle S^1(x^\#), S^1(y^\#) \rangle$ is in $STG_f$. ■

*Proof (of Lemma 1).* We prove the contrapositive. Take a trace $\langle s_0, \dots, s_p \rangle$ in $STG_f$ where $s_0 = x \in \gamma_s(\{x^\#\})$ and $s_p = y \in \gamma_s(\{y^\#\})$. By Theorem 1, all outgoing transitions in $f$ are preserved by the reduction. This implies that after removing duplicate consecutive states from its component-wise projection, $\beta_{\pi_T}(\langle s_0, \dots, s_p \rangle)$, the resulting trace is necessarily a trace in $STG_{\tilde{f}}$ starting in $x^\#$ and ending in $y^\#$. ■

*Proof (of Lemma 2).* By definition, if $\langle s, s' \rangle \in \beta_{\text{double}}(STG_f)$, either $\langle s, s' \rangle \in STG_f$ or $\langle \bar{s}, \bar{s}' \rangle \in STG_f$. If $\langle s, s' \rangle \in STG_f$, then $s' = s[i \leftarrow f_i(s)]$ for some $i \in \{1, \dots, n\}$ with $f_i(s) \neq s_i$. Letting $b = f_i(s)$, this tells us $b \in \beta_f(f_i)(s)$ and thus $\langle s, s' \rangle \in STG_{f^\#}$ necessarily. The second case follows similarly.

Conversely, if $\langle s, s' \rangle \in STG_{f^\#}$, $s' = s[i \leftarrow b]$ where $b \in \beta_f(f_i)(s)$ and $b \neq s_i$. By definition of $\beta_f(f_i)$, it follows that either $f_i(s) = b$ or $f_i(\bar{s}^r) = b$. The former implies $\langle s, s' \rangle \in STG_f$ and the latter that $\langle \bar{s}, \bar{s}' \rangle \in STG_f$. Either way, by construction $\beta_{\text{double}}(STG_f)$ will contain both transitions and thus in particular $\langle s, s' \rangle \in \beta_{\text{double}}(STG_f)$. ■
**Proof (of Lemma 3).** Notice that both $STG_f^\#$ and $STG_{\tilde{f}}$, are well-defined. We prove $STG_f^\# = STG_{\tilde{f}}$.

Take a transition $\langle \tilde{s}, \tilde{s}' \rangle \in STG_{\tilde{f}}$. Then $\tilde{s}' = \tilde{s}[i \leftarrow \beta_{\text{collapse}}^i \circ \beta_f(f_i)]$, with $\beta_{\text{collapse}}^i \circ \beta_f(f_i) \neq \tilde{s}_i$. Then $f_i(s) = s'$ for some $s \in \gamma_s(\{\tilde{s}\})$ and some $s' \in \gamma_s(\{\tilde{s}'\})$ with $f_i(s) = \tilde{s}'_i \neq s_i = \tilde{s}_i$. As $\langle s, s' \rangle \in STG_f$, it follows that $\langle \tilde{s}, \tilde{s}' \rangle \in STG_f^\# = \beta_{\pi_S} \circ \beta_{\text{double}}(STG_f)$.

Conversely, take a transition $\langle \tilde{s}, \tilde{s}' \rangle \in STG_f^\# = \beta_{\pi_S} \circ \beta_{\text{double}}(STG_f)$, then $\langle s, s' \rangle \in STG_f$ for some $s \in \gamma_s(\{\tilde{s}\})$ and some $s' \in \gamma_s(\{\tilde{s}'\})$. That is, there exists $s' = s[i \leftarrow f_i(s)]$ with $f_i(s) = \tilde{s}'_i \neq s_i = \tilde{s}_i$ for some $i < n$. This implies that $f_i(s) \in \beta_{\text{collapse}}^i \circ \beta_f(f_i)(\tilde{s})$, and thus $\langle \tilde{s}, \tilde{s}' \rangle \in STG_{\tilde{f}}$. ■

**Proof (of Theorem 4).** Towards a contradiction, suppose $\exists \tilde{s} \in \mathbb{B}^{n-1}$ and $\exists i < n$ such that $\tilde{f}_i(\tilde{s}) \neq \tilde{f}_i'(\tilde{s})$.

If $\tilde{f}_i(\tilde{s}) = \tilde{s}_i$ then $\tilde{f}_i'(\tilde{s}) = 1 - \tilde{s}_i$ and there is an outgoing transition affecting $s_i$ from $\tilde{s}$ in $STG_{\tilde{f}}$. By Theorem 3, there exists an outgoing transition from some state in $\gamma_s(\{\tilde{s}\})$ in $STG_f$ that gets projected onto that transition. Thus by Theorem 1, that same transition must also appear in $STG_{\tilde{f}}$ and thus $\tilde{f}_i(\tilde{s}) \neq \tilde{s}_i$, a contradiction.

Following a similar reasoning, if $\tilde{f}_i(\tilde{s}) = 1 - \tilde{s}_i$, by Theorem 2, there is an outgoing transition from a state in $\gamma_s(\{\tilde{s}\})$ in $STG_f$. By Theorem 3, this transition must appear in $STG_{\tilde{f}}$, and thus $\tilde{f}_i'(\tilde{s}) = 1 - \tilde{s}_i \neq \tilde{s}_i$, a contradiction. ■

**Proof (of Lemma 4).** The result follows by noticing that every transition in $\beta_{\text{rdup}} \circ \beta_{\pi_T}(t)$ is the projection of a transition in $STG_f$ and thus by Theorem 1, the obtained trace is necessarily a possible trace of $\tilde{f}$. ■

The next lemma states that projecting and then deleting duplicate consecutive states yields the same result as first compressing all consecutive elements belonging to the same equivalence class into a single element in the equivalence class and then projecting out the reduced component. It is just an auxiliary lemma that allows us to prove Theorem 5. Because our traces are always finite, its proof is immediate.

**Lemma 9.** $\forall t \in \mathcal{T}, \beta_{\text{rdup}} \circ \beta_{\pi_T}(t) = \beta_{\pi_T} \circ \beta_{\text{osci}}(t)$.

**Proof (of Theorem ??).** Fixing an arbitrary $x \in \mathcal{T}$, we prove both $[x]_\sim \equiv \rho_\pi \circ \rho_{\text{osci}}(\{x\})$ and $[x]_\sim \equiv \rho_{\text{osci}} \circ \rho_\pi(\{x\})$, thus establishing the operators commute for singletons.

The theorem statement then follows for an arbitrary set $X \in \wp(\mathcal{T})$ by:

$$ \rho_\pi \circ \rho_{\text{osci}}(X) = \bigcup_{x \in X} \rho_\pi \circ \rho_{\text{osci}}(\{x\}) = \bigcup_{x \in X} \rho_{\text{osci}} \circ \rho_\pi(\{x\}) = \rho_{\text{osci}} \circ \rho_\pi(X). $$

**▶ [x]^dplcs ≡ ρ_π ∘ ρ_{osci}(\{x\}):**

(C) Take some $t \in [x]_\sim$, then $\beta_{\text{rdup}} \circ \beta_{\pi_T}(t) = \beta_{\text{rdup}} \circ \beta_{\pi_T}(x)$ by definition and thus $\beta_{\pi_T} \circ \beta_{\text{osci}}(t) = \beta_{\pi_T} \circ \beta_{\text{osci}}(x)$ by Lemma 9. This tells us $\beta_{\text{osci}}(x)$ and $\beta_{\text{osci}}(t)$ disagree at most on the last (the reduced) component of each state.
From this remark it follows that $\exists t' : (\beta_{\text{osci}}(t') = \beta_{\text{osci}}(x)) \land (\beta_{\pi_{\tau}}(t) = \beta_{\pi_{\tau}}(t'))$. That is, while trace $t'$ agrees with $t$ in length, they may disagree on the last component of each state. On the other hand, $t'$ and $x$ may disagree on length, but agree on the last component after collapsing consecutive states in the same equivalence class. For states where $t$ and $t'$ disagree on the last component, $t'$ agrees with (its corresponding state in) $x$. By definition, this means $t \in \rho_{\pi}(\{t'\})$ and $t' \in \rho_{\text{osci}}(\{x\})$ and thus $t \in \rho_{\pi} \circ \rho_{\text{osci}}(\{x\})$.

(2) Now take $t \in \rho_{\pi} \circ \rho_{\text{osci}}(\{x\})$. By definition $\exists t' \in \rho_{\text{osci}}(\{x\}) : \beta_{\pi_{\tau}}(t') = \beta_{\pi_{\tau}}(t)$, but $t' \in \rho_{\text{osci}}(\{x\})$ means $\beta_{\text{osci}}(t') = \beta_{\text{osci}}(x)$. By applying Lemma 9 twice, we have $\beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(t) = \beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(t) = \beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(t') = \beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(t') = \beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(x)$, as desired.

► $[x] \sim \rho_{\text{osci}} \circ \rho_{\pi}(\{x\})$:

(1) Take some $t \in [x]$, then $\beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(t) = \beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(x)$ by definition and thus $\beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(t) = \beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(x)$ by Lemma 9, which again tells us that $\beta_{\text{osci}}(t)$ and $\beta_{\text{osci}}(x)$ disagree at most on the last component of each state.

This time we instead find a trace $t'$ such that $\beta_{\text{osci}}(t') = \beta_{\text{osci}}(t)$, meaning $t'$ agrees with $t$ on the last component of each state after collapsing oscillations to their first state, but such that $t'$ agrees with $x$ on length, $\beta_{\pi_{\tau}}(t) = \beta_{\pi_{\tau}}(x)$. Putting these properties together, we have that $t' \in \rho_{\pi}(x)$ and that $t \in \rho_{\text{osci}}(t')$ and thus $t \in \rho_{\text{osci}} \circ \rho_{\pi}(\{x\})$.

(2) Taking some $t \in \rho_{\text{osci}} \circ \rho_{\pi}(\{x\})$, by definition $\exists t' \in \rho_{\pi}(\{x\}) : \beta_{\text{osci}}(t') = \beta_{\text{osci}}(t')$ and thus by using Lemma 9 twice again, $\beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(t) = \beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(t) = \beta_{\pi_{\tau}} \circ \beta_{\text{osci}}(t') = \beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(t') = \beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}(x)$. ■

## C Proof Appendix for Section 4

As per usual, we assume the reduced component to be the last component to avoid index mismatching. To reason back and forth between original and reduced STGs, we need a way to interpret transitions with Hamming distance two.

**Definition 21.** Identifying transitions with the elements of $\mathcal{T}_2$, we define function $\gamma_{2\text{-to-1}} : \wp(\mathcal{T}_2) \to \wp(\mathcal{T}_2)$ as:

$$ \gamma_{2\text{-to-1}}^t(T) = \{\langle s, s' \rangle \in T \mid \Delta^n(\langle s, s' \rangle) = 1\} \cup \\ \cup \{\langle s, \bar{s} \rangle \mid \langle s, s' \rangle \in T \land \Delta^n(\langle s, s' \rangle) = 2\} \\ \cup \{\langle \bar{s}, s' \rangle \mid \langle s, s' \rangle \in T \land \Delta^n(\langle s, s' \rangle) = 2\} $$

Given a set of transitions $T$, function $\gamma_{2\text{-to-1}}$ keeps the asynchronous transitions in $T$ and decouples any fused transition in $T$ back into asynchronous transitions.

*Proof (of Theorem 9).* Let $\beta_{\text{rdup}}^{\pi_{\tau}}$ denote the composition $\beta_{\text{rdup}} \circ \beta_{\pi_{\tau}}$. By construction,

$$ \text{lfp}(\mathbb{F}_{\beta_{\pi_S} \circ \beta_{\text{valid}}(STG_f)})(\tilde{S}_0) = \beta_{\pi_{\tau}}(\text{lfp}(\mathbb{F}_{\beta_{\text{valid}}(STG_f)})(S_0)), \quad (3) $$
as every transition in $\beta_{\pi_S} \circ \beta_{\text{valid}}(\text{STG}_f)$ is a projection of a transition in $\beta_{\text{valid}}(\text{STG}_f)$ and these transitions always differ in a component different from the projected component.

Applying $\beta_{\text{rdup}}^{\pi_T}$ to both sides of Theorem 8, yields:

$$ \beta_{\text{rdup}}^{\pi_T}(\mathcal{V}_f) = \beta_{\text{rdup}}^{\pi_T}(\gamma_{2-\text{to}-1}(\mathbf{lfp}(\mathbb{F}_{\beta_{\text{valid}}(\text{STG}_f)})(\mathcal{S}_0))). $$

As $\beta_{\text{rdup}}^{\pi_T}$ removes consecutive duplicate states and $\gamma_{2-\text{to}-1}$ introduces transitions in the trace whose projection is the same state, their effects interplay and

$$ \beta_{\text{rdup}}^{\pi_T}(\mathcal{V}_f) = \beta_{\text{rdup}}^{\pi_T}(\gamma_{2-\text{to}-1}(\mathbf{lfp}(\mathbb{F}_{\beta_{\text{valid}}(\text{STG}_f)})(\mathcal{S}_0))) = \beta_{\pi_T}(\mathbf{lfp}(\mathbb{F}_{\beta_{\text{valid}}(\text{STG}_f)})(\mathcal{S}_0)), $$
from which our result follows by the initial remark (3). ■

*Proof (of Theorem 10).* We shorten $\mathbf{lfp}(\mathbb{F}_{\beta_{\pi_S} \circ \beta_{\text{valid}}(\text{STG}_f)})(\tilde{\mathcal{S}}_0)$ to $\mathbf{lhs}$ (for left-hand-side), and prove both inclusions by contradiction. For presentation purposes, we also drop the superscript $n$ from the representative state $\mathcal{R}^n$.

Recall that for Naldi's reduction $\tilde{f}_i$ at state $\tilde{s}$ is obtained by $\tilde{f}_i(\tilde{s}) = f_i(\mathcal{R}(\tilde{s}))$. By Kleene's fixed-point Theorem, $\mathbf{lhs} = \bigcup_{n \in \mathbb{N}_0} \mathbb{F}_{\beta_{\pi_S} \circ \beta_{\text{valid}}(\text{STG}_f)}^n(\tilde{\mathcal{S}}_0)$, and therefore every trace in $\mathbf{lhs}$ is of the form of $\langle \tilde{s}_0, \dots, \tilde{s}_k \rangle$ for some $k \in \mathbb{N}_0$ with every $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle \in (\beta_{\pi_S} \circ \beta_{\text{valid}})(\text{STG}_f)$.

Towards a contradiction, assume there is a trace $T'$ in $\mathbf{lhs}$ such that $T'$ is not in $T_{\tilde{f}}$, then there is some transition $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle \in T'$ that is not of the form $\tilde{s}_{i+1} = \tilde{s}_i[j \leftarrow \tilde{f}_j(\tilde{s}_i)] = \tilde{s}_i[j \leftarrow f_j(\mathcal{R}(\tilde{s}_i))]$ where $j$ is the component $\tilde{s}_i$ and $\tilde{s}_{i+1}$ differ on.

By equality (3) at the beginning of the proof of Theorem 9, every trace in $\mathbf{lhs}$ is the image under $\beta_{\text{rdup}}^{\pi_T} = \beta_{\text{rdup}} \circ \beta_{\pi_T}$ of some trace $T \in \mathcal{V}_f$ which therefore implies every transition in $T'$ is the projection of an outgoing transition from a representative state, which forces the existence of a transition $\langle \mathcal{R}(\tilde{s}_i), s_{i+1} \rangle$ such that $\beta_{\pi_T}(\langle \mathcal{R}(\tilde{s}_i), s_{i+1} \rangle) = \langle \tilde{s}_i, \tilde{s}_{i+1} \rangle$ with $s_{i+1} = \mathcal{R}(\tilde{s}_i)[j \leftarrow f_j(\mathcal{R}(\tilde{s}_i))]$ thus making $\tilde{s}_{i+1} = \beta_{\pi_S}(s_{i+1})$ of the form $\tilde{s}_{i+1} = \beta_{\pi_S}(\mathcal{R}(\tilde{s}_i)[j \leftarrow f_j(\mathcal{R}(\tilde{s}_i))]) = \tilde{s}_i[j \leftarrow f_j(\mathcal{R}(\tilde{s}_i))] = \tilde{s}_i[j \leftarrow \tilde{f}_j(\tilde{s}_i)]$, a contradiction.

For the opposite inclusion, suppose there is a trace $T' \in T_{\tilde{f}}$ such that $T' \notin \mathbf{lhs}$, then there is a transition $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle \in T'$ such that $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle \notin \beta_{\pi_S} \circ \beta_{\text{valid}}(\text{STG}_f)$. As $T'$ is duplicate-free, every transition $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle$ in $T'$ is of the form $\tilde{s}_{i+1} = \tilde{s}_i[j \leftarrow \tilde{f}_j(\tilde{s}_i)] = \tilde{s}_i[j \leftarrow f_j(\mathcal{R}(\tilde{s}_i))] = \beta_{\pi_S}(\mathcal{R}(\tilde{s}_i)[j \leftarrow f_j(\mathcal{R}(\tilde{s}_i))])$ where $j$ is the component $\tilde{s}_i$ and $\tilde{s}_{i+1}$ differ on.

That is every transition in $T'$ is the projection of an outgoing transition from a representative state in the original model, which contradicts $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle \notin \beta_{\pi_S} \circ \beta_{\text{valid}}(\text{STG}_f)$ as this would force $\langle \tilde{s}_i, \tilde{s}_{i+1} \rangle$ to be the projection of an outgoing transition from a non-representative state, the transitions purged by $\beta_{\text{valid}}$ by construction. ■