# Reachability Analysis for Parametric Rule-Based Models

Jerome Feret, Rebecca Ghidini

► To cite this version:

Jerome Feret, Rebecca Ghidini. Reachability Analysis for Parametric Rule-Based Models. 23rd International Conference on Computational Methods in Systems Biology, CMSB 2025, François Fages; Sabine Péres, Sep 2025, Lyon, France. pp.21, 10.1007/978-3-032-01436-8_9. hal-05121555

HAL Id: hal-05121555

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

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
Reachability Analysis
for Parametric Rule-Based Models

Jérôme Feret¹[0000-0002-2601-2785] and Rebecca Ghidini¹[0009-0009-8117-2659]

DI ENS, École Normale Supérieure, PSL, CNRS, INRIA, Paris, France
{jerome.feret, rebecca.ghidini}@info.ens.psl.eu

**Abstract.** Biological system modeling is an iterative process where uncertainties may arise, especially in the early stages of the modeling. Static analysis tools are needed during each stage of the modeling to help modelers detect unexpected behaviors early by automatically inferring properties about the model. However, the rule-based modeling language Kappa and its static analysis tool KaSa currently lack support for incomplete models.

In this work, we extend Kappa to support incomplete models, where some rules are considered or not depending on the value of some boolean parameters. We also generalize the current reachability analysis of the static analyzer KaSa to these parametric models, establishing relationships between properties and parameter values. Finally, we implement and evaluate our approach on example models.

**Keywords:** Rule-based modeling · Formal methods · Abstract interpretation · Static analysis.

# 1 Introduction

During the modeling process of a biological system, the modeler faces choices and sometimes finds new or contradicting hypotheses. The applicability context of a given interaction is often not clear. Rule-based languages, such as Kappa [12] and BNGL [1] may help in this exploration process: they focus on mechanistic local interactions, which can be assembled as a collection of more or less dependent modules, each of them with different variants according to the modeling assumptions [2]. Static analysis is, then, useful to increase confidence in models by checking the coherence of their underlying assumptions [3]. In particular, the static analyzer KaSa [3] detects local properties of the occurrences of proteins in the biochemical species that may arise in a Kappa model. KaSa is also able to detect and prove when the condition of a given interaction is never realizable. However, static analyzers can usually be applied to fully specified models only. To improve their impact and spread their usage, static analyzers have to be applicable at the early phase of modeling.

In this paper, we extend the static analyzer KaSa to cope with parametric rule-based models, where some parts of the model are allowed to be parameterized with some Boolean predicates. The parameterized parts are considered
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** Graphical representation of the proteins A, B and C. The protein A is represented by an orange square with its sites x, y and z. The protein B is a blue circle with one site, called t. The protein C is a green diamond with one site, called s. Each site is free (i.e., not bound to another site), which is represented by the symbol $\neg$.</figcaption></figure>

to be enabled when the parameters are true and are ignored otherwise. Then, the analysis establishes a relationship between certain biochemical products and the value that the Boolean predicates need to have in order for the products to be reachable by the model. The scalability of our approach relies on the use of binary decision diagrams [6] that are used to encode both Boolean valuations and local properties. The soundness of the approach is established by means of the abstract interpretation framework [7].

We have tested our analysis on several models of the literature, while considering some of their interaction rules to be optional. The one with the largest number of rules is a model of protein-protein interactions in yeast [13]. It is made of 232 Kappa rules, among which we considered the first 60 to be optional (hence corresponding to 2⁶⁰ versions of the model). Our analysis was completed in less than 11 seconds on a 2020 16 GB MacBook Pro. Memory usage is the main limitation of our analysis to go beyond this number of Boolean parameters.

*Related works.* Abstract interpretation [7] has been widely utilized to infer biological model properties. It is used to derive static analysis of Bioambients to infer their hierarchical structure [15] and their temporal behavior in [20]. In the context of Boolean networks and logical modeling, it has been applied in [14] to derive the Boolean semantics of BIOCHAM. It has also been used to abstract the behavior of Process Hitting system in [24], and more general automaton networks in [18,19].

Our analysis is based on the one that is presented in [11,17] and implemented in KaSa [3]. In the present contribution, this analysis is extended to cope with parametric models and establish a relationship between reachable patterns and the valuation of the model parameters.

## 2 Case Study

We motivate our work by means of a not fully-specified model. We will use it as a running example throughout this paper.

The model consists of three types of protein, called A, B and C. The protein A has three binding sites, called x, y and z. The protein B has only one site t and the protein C has a site s. The three proteins are graphically represented as shown in Fig. 1. The sites x and y on the right of A can bind to the instances of B on its binding site t. The site z can bind to the site s of an instance of C only if both its other sites are already bound. The three rules modeling this behavior are shown in Fig. 2.
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** The rules $r_1$ and $r_2$ describe how the protein A can bind to the protein B through either the site x (in $r_1$) or the site y (in $r_2$). The site z of A can bind to s of C only if the other two sites are already bound. In rule $r_3$ it is not specified to which protein x and y are bound, the dangling edge describes any potential binding partner.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>**Fig. 3.** The rules $r'_1$ and $r'_2$ are equivalent to $r_1$ and $r_2$, respectively, except that there is an additional assumption that x and y are in conflict. Therefore, each of these sites can only bind if the other one is free.</figcaption></figure>

Our goal is to compare the previously described model with an equivalent model that has an additional hypothesis: the sites x and y are in conflict. This means that site x can only bind to another site if y is free, and conversely. In this version of the model, the two first rules are replaced by the ones that are shown in Fig. 3. We want to analyze both versions of the two model at once. Thus, we introduce a Boolean parameter b to the analysis, which represents the question “are x and y in conflict?”. The rules $r_1$ and $r_2$ are enabled when b is false, while $r'_1$ and $r'_2$ are enabled when b is true. Rule $r_3$ is always enabled. The analysis that we present in this paper automatically infers that the site z of an instance of A may be bound only when the sites x and y are not considered to be in conflict.

# 3 Kappa

In this section, we introduce the syntax and the operational semantics of a small core of the language Kappa. In particular, we do not describe sites with internal states, protein creation, protein degradation, and side effects. The formalization of these concepts for the full language may be found in [12,16].

## 3.1 Signature

Firstly, we define the signature of a model.

**Definition 1 (signature).** A signature $\Sigma$ is a triple $(\Sigma_{ag}, \Sigma_{st}, \Sigma^{lnk})$ where:
1. $\Sigma_{ag}$ is a finite set of agent types,
2. $\Sigma_{st}$ is a finite set of site identifiers;
3. $\Sigma^{lnk} : \Sigma_{ag} \to \wp(\Sigma_{st})$ is a site map.

Agent types in $\Sigma_{ag}$ denote agents of interest, as kinds of proteins. A site identifier in $\Sigma_{st}$ represents an identified locus for capability of interactions. Each agent type $A \in \Sigma_{ag}$ is associated with a set of sites $\Sigma^{lnk}(A)$ which may be linked.
<figure><img src="image_5.png" /><figcaption>Fig. 4. Example of a site graph.</figcaption></figure>

*Example 1.* We define the signature for our case study as: 1. $\Sigma_{ag}$ is given by $\{A, B, C\}$; 2. $\Sigma_{st}$ is given by $\{x, y, z, t, s\}$; 3. $\Sigma^{lnk}$ is given by $[A \mapsto \{x, y, z\}, B \mapsto \{t\}, C \mapsto \{s\}]$.

## 3.2 Site-graphs

Site-graphs describe both patterns and biomolecular species. Their nodes are typed agents with some sites which bear binding states.

**Definition 2 (site-graph).** A site-graph is a tuple $(\mathcal{A}_G, \text{type}_G, S_G, \mathcal{L}_G)$ where:
1. $\mathcal{A} \subseteq \mathbb{N}$ is a finite set of agent identifiers, 2. type : $\mathcal{A} \to \Sigma_{ag}$ is a function mapping each agent identifier to the type of the corresponding agent, 3. $S$ is a subset of the set $\{(n, i) \mid n \in \mathcal{A}, i \in \Sigma^{lnk}(\text{type}(n))\}$, 4. $\mathcal{L}$ is a function between the set $S$ and the set $S \cup \{\mathcal{D}, -\}$ such that for any two sites $(n, i), (n', i') \in S$, we have $(n', i') = \mathcal{L}(n, i)$ if and only if $(n, i) = \mathcal{L}(n', i')$.

The set $S$ denotes the set of binding sites. Whenever $\mathcal{L}(n, i) = \mathcal{D}$, the site $(n, i)$ is free. If $\mathcal{L}(n, i) = -$, the site $(n, i)$ is bound to an unspecified site. Whenever $\mathcal{L}(n, i) = (n', i')$ (and hence $\mathcal{L}(n', i') = (n, i)$), the sites $(n, i)$ and $(n', i')$ are bound together.

For a site-graph $G$, we write as $\mathcal{A}_G$ its set of agent identifiers, $\text{type}_G$ its typing function, $S_G$ its set of sites, and $\mathcal{L}_G$ its set of links.

A biomolecular species is a connected site-graph in which each site is documented (i.e. for every agent identifier $n \in \mathcal{A}$ and every site identifier $i \in \Sigma^{lnk}(\text{type}(n))$, the site $(n, i)$ is in the set $S_G$ and $\mathcal{L}(n, i) \neq -$). We denote as $BS_\Sigma$ the set of the biomolecular species in the signature $\Sigma$.

*Example 2.* Fig. 4 shows an example of a site graph $G$ that shows the proteins $C$ and $A$ that are bound to each other. It is not a biomolecular species, as it is not specified to which protein the two sites $x$ and $y$ are bound. The tuple $(\mathcal{A}_G, \text{type}_G, S_G, \mathcal{L}_G)$ is defined as: 1. $\mathcal{A}_G = \{1, 2\}$, 2. $\text{type}_G = [1 \mapsto C, 2 \mapsto A]$, 3. $S_G = \{(1, s), (2, x), (2, y), (2, z)\}$, 4. $\mathcal{L}_G = [(1, s) \mapsto (2, z), (2, x) \mapsto -$, $(2, y) \mapsto -$, $(2, z) \mapsto (1, s)]$.

## 3.3 Embeddings

Two site-graphs can be related by structure-preserving injective functions, which are called embeddings. The notion of embedding is defined as follows:

**Definition 3 (embedding).** An embedding $h$ from a site-graph $G$ into a site-graph $H$ is a function of agent identifiers $h : \mathcal{A}_G \to \mathcal{A}_H$ satisfying, for all agent identifiers $n, n' \in \mathcal{A}_G$, for all site identifiers $i \in \Sigma^{lnk}(\text{type}_G(n))$, $i' \in \Sigma^{lnk}(\text{type}_G(n'))$.
<figure><img src="image_6.png" /><figcaption>**Fig. 5.** Example of an embedding. The graph *G* can be embedded into *H* because it is a subgraph of *H*: the graph *H* contains all the agents and all the sites of *G*.</figcaption></figure>

$\Sigma^{\text{lnk}}(\text{type}_G(n'))$: 1. if $n \neq n'$, then $h(n) \neq h(n')$; 2. $\text{type}_G(n) = \text{type}_H(h(n))$; 3. if $(n, i) \in \mathcal{S}_G$, then $(h(n), i) \in \mathcal{S}_H$; 4. if $\mathcal{L}(n, i) = (n', i')$, then $\mathcal{L}_H(h(n), i) = (h(n'), i')$;

*Example 3.* An example of an embedding from a pattern into another one is depicted in Fig. 5. The agent *A* of the graph *G* is mapped to the agent *A* of the graph *H*. This is possible because no other agent was mapped to *A* (property 1) and the two agents have the same type (property 2) and the site *z* is present in the graph *H* (property 3).

**3.4 Rules**

Transformations between site-graphs are described by rules.

**Definition 4 (rule).** A rule is a pair of site-graphs $L \rightarrow R$ such that 1. $A_L = A_R$; 2. for all agent identifiers $n \in A_L$, $\text{type}_L(n) = \text{type}_R(n)$; 3. $S_L = S_R$; 4. for all sites $(n, i) \in S_L$, $\mathcal{L}_L(n, i) = - \Longleftrightarrow \mathcal{L}_R(n, i) = -$.

Since we consider neither agent creation, nor agent degradation, we can assume
that the agents on the left-hand side and on the right-hand side of a rule have
the same identifiers (constraint 1), with the same type (constraint 2) and the
same sites (constraint 3). We also assume that partially specified bounds cannot
be removed (constraint 4).

*Example 4.* Some examples of rules are given in Fig. 2 and Fig. 3. They describe under which conditions the proteins in the model can bind to other proteins.

**3.5 Rule refinements**

Rules may be more or less specific, which leads to the notion of rule refinement.

**Definition 5 (rule refinement).** A rule $L' \rightarrow R'$ is a refinement of a rule $L \rightarrow R$ if there exists a function $h$ from the agent identifiers of $L$, $A_L$, into the agent identifiers of $L'$, $A_{L'}$, that defines two embeddings respectively from $L$ to $L'$, and from $R$ to $R'$.

Intuitively, a refinement consists in inserting to the left-hand side and the
right-hand side of a rule exactly the same amount of information. It can be
equally defined by means of an embedding from the left-hand side or a right-
hand side of a rule to a pattern.
<figure><img src="image_7.png" /><figcaption>Fig. 6. Example of a reaction.</figcaption></figure>

*Example 5.* The rule $r_1'$ in Fig. 3 can be considered as a refinement of the rule $r_1$ in Fig. 2. They describe the same binding operation, but $r_1'$ has additional information on both sides of the rule, i.e. that the site *y* needs to be bound. Similarly, the rule $r_2'$ is a refinement of $r_2$.

Rule refinements are useful to define the notion of reaction, which is the cornerstone of the ordinary differential semantics of Kappa. A rule can be understood as a symbolic representation of a potentially infinite set of reactions among biomolecular species. Indeed, a reaction is a particular case of refinement in which the states of all the sites are fully specified. In the ordinary differential equation semantics of Kappa, only the reactions that preserve the disconnectedness in the left-hand side of the rule are considered.

**Definition 6 (reaction).** A reaction $L' \rightarrow R'$ is a refinement of a rule $L \rightarrow R$ by the embedding $\phi$ if and only if: 1. The state of all the sites in the pattern $L'$ are fully specified. 2. For each agent identifier *n* in the pattern $L'$, there exists an agent identifier *n'* in the same connected component that is the image by $\phi$ of an agent identifier in the pattern $L'$. 3. For each two agent identifiers *n*,*n'* in the pattern $L$ that do not belong to the same connected component, the agent identifiers $\phi(n)$ and $\phi(n')$ do not belong to the same connected component in the pattern $L'$ either.

We notice that a reaction is obtained by refining each connected component of the left-hand side of a rule into a biomolecular species. Neither connecting two connected components on the left-hand side (constraint 3), nor adding a new connected component is allowed (constraint 2). The right-hand side of a reaction is also a disjoint union of biomolecular species [9].

*Example 6.* The rules in Fig. 3 are not reactions, as the site *z* is not defined in the site-graphs. An example of a reaction that is a refinement of the rule $r_1$ is shown in Fig. 6.

Given a reaction $R$, we denote as *Reactants($R$)* (resp. *Products($R$)*)) the set of reactants (resp. products) of the reaction (that is to say the set of biochemical species occurring in its *lhs* (resp. *rhs*)).

# 4 Reachable Biomolecular Species in Parametric Models

A Kappa model consists of a pair ($\mathcal{I}$, $\mathcal{R}$) of a set $\mathcal{I}$ of initial biomolecular species and a set $\mathcal{R}$ of rules. In this section, we generalize Kappa models by potentially guarding the rules of the models and the biomolecular species in the initial
states with a Boolean formula. Then, we define the semantics of the model as a function that maps a Boolean valuation to a set of biomolecular species that may be constructed from the initial species by applying an arbitrary number of reactions induced by the rules available with this Boolean valuation.

The guards in front of the rules and initial biochemical species are Boolean formulas made up of Boolean predicates. Let $\Sigma_p$ be a set of possible predicate identifiers. A Boolean formula may be a constant true or false, an atomic predicate $p \in \Sigma_p$, or the application of a logical operator $\wedge$, $\vee$ or $\neg$ to other Boolean formulas.

$$F = true | false | p \in \Sigma_p | \neg F | F \wedge F | F \vee F$$

The set of rules $\mathcal{R}$ of a parametrized model contains tuples $(g, r)$ of a Boolean formula $g$ over the atomic predicates in $\Sigma_p$ and a rule $r$. Similarly, the initial state of the model is defined as a set $\mathcal{I}$ of tuples $(g, bs)$ of a Boolean formula $g$ and a biochemical species $bs$.

**Example 7.** As described in Section 2, we use an atomic predicate $b$ to indicate whether there is a conflict between the sites $x$ and $y$ or not. When $b$ is true, it means that there is a conflict, therefore the rules $r'_1$ and $r'_2$ are enabled. Otherwise, rules $r_1$ and $r_2$ are enabled. The rule $r_3$ is always enabled. Thus, the rule set of our example model is $\mathcal{R} = \{(b, r'_1), (b, r'_2), (\neg b, r_1), (\neg b, r_2), (true, r_3)\}$. The initial state $\mathcal{I}$ consists of the agents $A, B$ and $C$ that contain no links, as in Fig. 1, and they each have the guard true.

From now on, we assume without loss of generality that $\Sigma_p = \{b_1, \dots, b_n\}$ is a set of $n$ atomic predicates. Each atomic predicate can be assigned a value from the set $\mathbb{B} = \{0, 1\}$. A valuation for these atomic predicates is represented by a string $\rho \in \mathbb{B}^n$, where each digit of $\rho$ is the value of one of the predicates $\{b_1, \dots, b_n\}$. The Boolean value of the Boolean formula $g$ interpreted under the valuation $\rho \in \mathbb{B}^n$ is denoted as $\llbracket g \rrbracket^\rho$. $\llbracket g \rrbracket^\rho$ is defined inductively on the syntax of the formula $g$ is the classical way.

A parametric Kappa model can be instantiated by selecting a Boolean valuation $\rho \in \mathbb{B}^n$, and then by keeping only the rules and initial biochemical species for which the corresponding guard evaluates to true. Given a set $\mathcal{R}$ of tuples containing a formula and a rule, the set $\mathcal{R}_\rho = \{r \mid (g, r) \in \mathcal{R}, \llbracket g \rrbracket^\rho = 1\}$ is the set of rules whose guard evaluates to true under the valuation $\rho$. The set $\mathcal{I}_\rho = \{bs \mid (g, bs) \in \mathcal{I}, \llbracket g \rrbracket^\rho = 1\}$ contains the initial biochemical species that are present under a certain valuation $\rho$. Each parametric model $(\mathcal{I}, \mathcal{R})$ can thus be refined to a fully-specified model $(\mathcal{I}_\rho, \mathcal{R}_\rho)$ for a certain valuation $\rho$. We define as Reactions$_{\mathcal{R}_\rho}$ the set of reactions that are induced by some rule in the set $\mathcal{R}_\rho$.

**Example 8.** The model from Example 7 contains only one atomic predicate, therefore the possible valuations are 0 and 1. $\mathcal{R}_0 = \{r_1, r_2, r_3\}$ and $\mathcal{R}_1 = \{r'_1, r'_2, r'_3\}$ and $\mathcal{I}_0 = \mathcal{I}_1$, containing all the initial biochemical species.

Let $(\mathcal{I}, \mathcal{R})$ be a Kappa model. For a given valuation $\rho \in \mathbb{B}^n$ and a model $(\mathcal{I}, \mathcal{R})$, the function $F_\rho$ computes the biochemical species that are reachable by
applying one of the rules in $\mathcal{R}$ that are enabled by the valuation $\rho$.

$$ \mathbb{F}_{\rho} : \left\{ \begin{array}{c} \varphi(\mathcal{BS}_{\Sigma}) \to \varphi(\mathcal{BS}_{\Sigma}) \\ X \mapsto \mathcal{I}_{\rho} \cup \left\{bs' \mid \begin{array}{l} \exists R \in \text{Reactions}_{\mathcal{R}_{\rho}} \text{ such that} \\ \text{Reactants}(R) \subseteq X \text{ and } bs' \in \text{Products}(R) \end{array} \right\} \end{array} \right\}. $$

The operator $\mathbb{F}_{\rho}$ is a monotonic map over a complete lattice. Thus, by [26], it admits a least fixpoint. The least fixpoint $lfp \mathbb{F}_{\rho}$ is the set of reachable biochemical species of the model $(\mathcal{I}_{\rho}, \mathcal{R}_{\rho})$. The semantics of a model is then the function mapping each Boolean valuation $\rho \in \mathbb{B}^n$ to the set of reachable states $lfp(\mathbb{F}_{\rho})$. This semantics of a model can also be expressed as the least fixpoint of the function $\mathbb{G}$, defined as follows:

$$ \mathbb{G} : \left\{ \begin{array}{l} (\mathbb{B}^n \to \varphi(\mathcal{BS}_{\Sigma})) \to (\mathbb{B}^n \to \varphi(\mathcal{BS}_{\Sigma})) \\ \sigma \mapsto (\rho \mapsto \mathbb{F}_{\rho}(\sigma(\rho))) \end{array} \right\} $$

The operator $\mathbb{G}$ is also a monotonic map over a complete lattice (for set inclusion applied point-wisely) and thus it admits a least fixpoint. The least fixpoint $(lfp \mathbb{G}) : \mathbb{B}^n \to \varphi(\mathcal{BS}_{\Sigma})$ describes the semantics of the model, i.e. which biochemical species are reachable for each valuation. It holds that $(\rho \mapsto lfp \mathbb{F}_{\rho}) = (lfp \mathbb{G})$. This latter formulation is more convenient to derive the static analysis that is described in the next section.

# 5 Pattern Reachability Analysis

The set of biochemical species might be infinite, making it impossible to compute the least fixpoint of $\mathbb{G}$ in finite time. Even when the signature of the model only admits a finite number of different biochemical species, this computation may not scale because of the potentially large number of possible biochemical species and Boolean valuations. However, during the modeling process, it is important to gain insights about the model, to validate it or to identify potential unexpected behavior. These insights can be obtained by applying static analysis on the model. By statically analyzing the model, it is possible to prove the unreachable of certain biochemical species, without the overhead of computing the exact set of all reachable species.

This section describes a static analysis for parametric Kappa models, that derives a scalable and sound approximation of the set of reachable biochemical species for each potential parameterization of a model. It is a generalization of the static analysis methods for Kappa models described in [17]. As in [17], the analysis is based on the abstract interpretation framework and the set of reachable biochemical species is abstracted by means of a set of patterns of interest.

## 5.1 Patterns of Interest
<figure><img src="image_8.png" /><figcaption>Fig. 7. These six patterns are the patterns of interest $\mathcal{P}$ for our case study.</figcaption></figure>

Instead of determining which concrete biochemical species are reachable by the model, the analysis considers only a set $\mathcal{P}$ of patterns of interest and determines for each pattern, whether it can prove their unreachable or not. The patterns of $\mathcal{P}$ are connected, i.e. they contain only one connected component. The choice of the set $\mathcal{P}$ determines which property can be proven about the model. An example of such properties would be to determine the relationship between different sites of a protein or to determine if double bonds can be formed. In practice the set $\mathcal{P}$ will be computed automatically, by a syntactic pre-analysis of the model (see Section 7).

*Example 9.* For the Kappa model described in Section 2, we are interested in whether the site *z* can be bound, which depends on the states of the sites *x* and *y*. Therefore, the set $\mathcal{P}$ of patterns of interest is selected to be formed of six patterns, shown in Fig. 7. The first four patterns represent the possible states of the *x* and *y*. These are compared to the two possible states of the site *z*.

We propose to abstract a set $X \subseteq BS_\Sigma$ of biochemical species as the set of $\alpha_P(X)$ of the patterns of interest in $\mathcal{P}$ that occur in at least one biochemical species in the set $X$. Conversely, given a set $X^\sharp \subseteq \mathcal{P}$ of patterns, we denote as $\gamma_P(X^\sharp)$ the set of biochemical species that do not contain any occurrence of a pattern in the set $\mathcal{P} \setminus X^\sharp$. The functions $\alpha_P$ and $\gamma_P$ form a Galois connection $[7,8]$ (i.e. the properties 1. $\alpha_P(X) \subseteq X^\sharp$; 2. $X \subseteq \gamma_P(X^\sharp)$; are equivalent).

## 5.2 Pattern Production

As shown in [8], the best abstract counterpart of the function $F_\rho$ is the function $\alpha_P \circ F_\rho \circ \gamma_P$. However, its computation requires to reason over the biochemical species. We propose to define a less precise abstract counterpart of $F_\rho$ that operates directly over the patterns of interest. To address this point, we investigate how a pattern of interest may be produced when applying a rule $r$. This requires an overlap between the pattern $\mathcal{P}$ and the right-hand side of the rule $r$. In such a case, the rule may be specialized by inserting on both sides of the rule any information that is present in the pattern and not in the right-hand side of the rule.

*Example 10.* In our example, an overlap between the right-hand side of the rule $r_1$ and the pattern made of an instance of the protein *A* with its site *x* bound to an unspecified target, its site *y* free, and its site *z* undocumented, is depicted in Fig. 8. It defines a right refinement of this rule, specialized to the production of this pattern. The red sites represent the information that was added to the left-hand side and the right-hand side of the rule $r_1$ to specialize this rule.
<figure><img src="image_9.png" /><figcaption>Fig. 8. The specialization of rule $r_1$ to the production of a specific pattern.</figcaption></figure>

Given an overlap between a pattern of interest and the right-hand side of a rule, and the corresponding the specialized rule, we have to consider the pattern as reachable whenever we cannot prove that the left-hand side of the specialized rule is unreachable. This reasoning can be done at different levels of accuracy, hence leading to less and more precise analyses. To leave the choice of accuracy open, we introduce a decision procedure $dp$, that maps each pattern $Q$ (which is not necessarily in the set $\mathcal{P}$ and not necessarily connected) to a set $dp(Q)$ of subsets of $\mathcal{P}$. The set $dp(Q)$ has to satisfy the following requirement: for any set $X^\sharp \subseteq \mathcal{P}$ of patterns of interest, if there exists a biochemical species $bs \in \gamma_{\mathcal{P}}(X^\sharp)$ that contains an occurrence of the pattern $Q$, then there exists a set of patterns $Cl \in dp(Q)$ such that $Cl \subseteq X^\sharp$.

*Example 11.* An example of such a decision procedure is the function which maps each pattern $Q$ to the singleton made of the patterns of interest in the set $\mathcal{P}$ that occur in $Q$.

Given the construction to specialize rules to produce certain patterns and given the decision procedure $dp(Q)$, we can now introduce inference rules, or Horn clauses, to specify under which condition our analysis will consider a pattern of interest to be reachable. Let $P \in \mathcal{P}$ be a pattern of interest, $L'$ the left-hand side of the refinement of a rule $r$ due to an overlap between the pattern $P$ and the right-hand side of the rule $r$, and let $\{P_1, \dots, P_k\} \in dp(L')$. We cannot prove, at our level of abstraction, that $P$ is not reachable, whenever we cannot prove that at least one pattern among $P_1, \dots, P_k$ is not reachable either. Thus, we have to consider that the pattern $P$ is potentially reachable if $P_1, \dots, P_k$ are potentially reachable. This is denoted by the Horn clause: $P := P_1, \dots, P_k$. Given a Boolean valuation $\rho$, we denote by $\mathcal{H}_{dp,\rho}$ the set of all the Horn clauses that can be derived this way by using a refinement of a rule $r$ in $\mathcal{R}_{\rho}$.

*Example 12.* Given the set of patterns of interest $\mathcal{P}$ from Fig. 7, we build the Horn clauses for the rules $r_1, r'_1$ and $r_3$. They are visualized in Fig. 9. Each Horn clause is annotated with the rule that has been used to induce it. The first Horn clause comes from the specialization of the rule $r_1$ that is depicted in Fig. 8. The other ones are constructed the same way.

We have now all the ingredients to define a less precise counterpart to the function $\mathbb{F}_{\rho}$. Given a Boolean valuation $\rho \in \mathbb{B}^n$, we define the function $\mathbb{F}_{\rho}^\sharp$ as
<figure><img src="image_10.png" /><figcaption>Fig. 9. Four examples of Horn clauses used by the reachability analysis. They correspond to the rules $r_1, r'_1$ and $r_3$. Each Horn clause states that if the analysis reaches all the patterns on the right-hand side, then the pattern on the left-hand side is considered as reachable.</figcaption></figure>

follows:

$$ \mathbb{F}_{\rho}^{\sharp} : \left\{ \begin{array}{l} \wp(\mathcal{P}) \to \wp(\mathcal{P}) \\ X^{\sharp} \mapsto \alpha_{\mathcal{P}}(\mathcal{I}_{\rho}) \cup \left\{ P' \mid \begin{array}{l} \exists P' := P_1, \dots, P_k \in \mathcal{H}_{dp,\rho} \text{ such that} \\ \{P_1, \dots, P_k\} \subseteq X^{\sharp} \end{array} \right. \end{array} \right\}. $$

By construction, the inclusion $[\alpha_{\mathcal{P}} \circ \mathbb{F}_{\rho} \circ \gamma_{\mathcal{P}}](X^{\sharp}) \subseteq \mathbb{F}_{\rho}^{\sharp}(X^{\sharp})$ is satisfied, for any set $X^{\sharp}$ of patterns of interest. Since $\mathbb{F}_{\rho}^{\sharp}$ is monotonic over the complete lattice $\wp(\mathcal{P})$, thus [7], it has a least fixpoint $lfp \mathbb{F}_{\rho}^{\sharp}$ and $lfp \mathbb{F}_{\rho} \subseteq \gamma_{\mathcal{P}}(lfp \mathbb{F}_{\rho}^{\sharp})$.

## 5.3 Reachability Analysis for Parametric Models

Computing the least fixpoint of the function $\mathbb{F}_{\rho}^{\sharp}$ for every Boolean valuation $\rho \in \mathbb{B}^n$ would not scale. In this section, we compute instead a relationship between each pattern of interest and the set of the Boolean valuations for which we cannot prove this pattern to be unreachable.

To this aim, we lift the abstraction and the concretization to act on functions from $\mathbb{B}_n$ to $\wp(\mathcal{BS}_{\Sigma})$, respectively, $\wp(\mathcal{P})$. Given a function $\sigma : \mathbb{B}^n \to \wp(\mathcal{BS}_{\Sigma})$, the lifted abstraction is defined as $\alpha'_{\mathcal{P}}(\sigma) = (\rho \mapsto \alpha_{\mathcal{P}}(\sigma(\rho)))$. Similarly, given the function $\sigma^{\sharp} : \mathbb{B}^n \to \wp(\mathcal{P})$, the lifted concretization is defined as $\gamma'_{\mathcal{P}}(\sigma^{\sharp}) = (\rho \mapsto \gamma_{\mathcal{P}}(\sigma^{\sharp}(\rho)))$. Additionally, we introduce the function $\Phi$ that maps any function $f$ from $\mathbb{B}^n$ to $\wp(\mathcal{P})$, to the function from $\mathcal{P}$ to $\wp(\mathbb{B}^n)$ that is defined as follows:

$$ \Phi(f) : \left\{ \begin{array}{l} \mathcal{P} \to \wp(\mathbb{B}^n) \\ P \mapsto \{\rho \in \mathbb{B}^n \mid P \in f(\rho)\}. \end{array} \right. $$

The function $\Phi$ is monotonic and bijective. We denote as $\Phi^{-1}$ its inverse. Our goal is to compute, for each pattern of interest $P \in \mathcal{P}$, a super-set of the set of Boolean valuations $\Phi(\alpha'_{\mathcal{P}}(lfp \mathbb{G}))(P)$, that is to say to a super-set of the Boolean valuation for which the pattern $P$ may be reachable.

The pair of functions $\Phi \circ \alpha'_{\mathcal{P}}$ and $\gamma'_{\mathcal{P}} \circ \Phi^{-1}$ form a Galois connection. That is to say that for every function $\sigma$ from the set $\mathbb{B}^n$ to the set $\wp(\mathcal{BS}_{\Sigma})$ and every function $\sigma^{\sharp}$ from the set $\mathcal{P}$ to the set $\wp(\mathbb{B}^n)$, both following assertions: 1. for any pattern of interest $P \in \mathcal{P}$, $\Phi(\alpha'_{\mathcal{P}}(\sigma))(P) \subseteq \sigma^{\sharp}(P)$, 2. for any Boolean valuation
<figure><img src="image_11.png" /><figcaption>Fig. 10. Horn clauses of the parametric model for the rules $r'_1$ and $r_3$.</figcaption></figure>

$\rho \in \mathbb{B}^n$, $\sigma(\rho) \subseteq \gamma'_P(\Phi^{-1}(\sigma^\#))(\rho)$, are equivalent. As a consequence, the function $\Phi \circ \alpha'_P \circ \mathbb{G} \circ \gamma'_P \circ \Phi^{-1}$ is the best counterpart to the function $\mathbb{G}$ in the abstract domain $\mathcal{P} \to \wp(\mathbb{B}^n)$. Since it is monotonic, it has a least fixpoint and, by [7], $(\lfloor \mathbb{G} \rfloor)(\rho) \subseteq \gamma'_P(\Phi^{-1}(\lfloor \mathbb{G} \rfloor[\Phi \circ \alpha'_P \circ \mathbb{G} \circ \gamma'_P \circ \Phi^{-1}]))(\rho)$.

We can abstract the function $\mathbb{G}$ further, by using the decision procedure $dp$. For this, we annotate each Horn clause coming from the decision procedure $dp$ with the guard of the rule that has been used to generate it. Formally, this amounts to define the set $\mathcal{H}_{dp}$ as the set of the pairs $(g, Cl)$ such that: 1. there exists a rule $r$ such that $(g, r) \in \mathcal{R}$; 2. $Cl$ is a Horn clause derived by refining the rule $r$ and applying the decision procedure $dp$ (as defined in Section 5.2).

*Example 13.* The annotation of the Horn clauses for rules $(b, r'_1)$ and $(\mathit{true}, r_3)$ of Fig. 9 are shown in Fig. 10. Similarly, the annotation of the other Horn clauses can be derived from the remaining rules of the model.

We consider the function $\mathbb{G}^\#$ that is defined as follows:

$$ \left\{ \begin{array}{l} (\mathcal{P} \to \wp(\mathbb{B}^n)) \to (\mathcal{P} \to \wp(\mathbb{B}^n)) \\ f^\# \mapsto \left( P \mapsto \mathit{init}^\#(P) \cup \bigcup_{P :=_g P_1, \dots, P_k \in \mathcal{H}_{dp}} \phi(f^\#, g, \{P_1, \dots, P_k\}) \right). \end{array} \right. $$

where:

1. $\mathit{init}^\#(P) = \{\rho \in \mathbb{B}^n \mid (g, bs) \in \mathcal{I} \text{ such that } P \text{ occurs in } bs \text{ and } \llbracket g \rrbracket^\rho = 1\}$;

2. $\phi(f^\#, g, \{P_1, \dots, P_k\}) = (\{\rho \in \mathbb{B}^n \mid \llbracket g \rrbracket^\rho = 1\} \cap f^\#(P_1) \cap \dots \cap f^\#(P_k))$.

Intuitively, the function $\mathbb{G}^\#$ collects, for each pattern of interest, the Boolean valuations coming from the initial biochemical species and the ones coming from the Horn clauses. For the former, we consider only the guards associated to the biochemical species that contain an occurrence of the pattern of interest. For the latter, we scan the set of the Horn clauses which may be used to deduce this pattern. Given such a Horn clause, we take into account the guard of the corresponding rule and the sets of Boolean valuations that are associated (in the current abstract state) to the pattern in the premise of this Horn clause.

The function $\mathbb{G}^\#$ is a sound counterpart to the function $\mathbb{G}$: for any function $\sigma : \mathcal{P} \to \wp(\mathbb{B}^n)$ and any pattern of interest $P \in \mathcal{P}$, $([\Phi \circ \alpha'_P \circ \mathbb{G} \circ \gamma'_P \circ \Phi^{-1}](\sigma))(P) \subseteq (\mathbb{G}^\#(\sigma))(P)$. Since it is monotonic, it has a least fixpoint. By [7,8], for any Boolean valuation $\rho \in \mathbb{B}^n$, we have: $[\lfloor \mathbb{G} \rfloor](\rho) \subseteq \gamma'_P(\Phi^{-1}(\lfloor \mathbb{G} \rfloor^\#))(\rho)$. It follows the overall soundness of our analysis:

**Theorem 1 (Soundness).** For any pattern of interest $P \in \mathcal{P}$ and any Boolean valuation $\rho \in \mathbb{B}^n$, if there exists a biochemical species $bs \in \mathcal{BS}_\Sigma$, such that $P$ occurs in $bs$ and $bs \in [\lfloor \mathbb{G} \rfloor](\rho)$, then $\rho \in [\lfloor \mathbb{G}^\# \rfloor](P)$.
This theorem demonstrates that if the result of the analysis does not map a pattern to a certain valuation, then for this valuation no biochemical species which contains this pattern is reachable in the concrete semantics of the model. This is only a one-way implication because we compute the reachability on an abstraction instead of the concrete biochemical models.

*Example 14.* The result of the analysis on our example maps the patterns where $z$ is bound and the one where $x$ and $y$ are both bound to the set of the single valuation $\{0\}$ and each of the other four patterns to the set $\{0, 1\}$. Therefore, we conclude that $z$ can only be bound if there is no conflict between $x$ and $y$.

We now wonder about the accuracy of the result. We notice that, for any abstract state $\sigma^\# : \mathcal{P} \to \wp(\mathbb{B}^n)$, the function $\mathbb{G}^\#(\sigma^\#)$ can also be expressed as $\Phi([\rho \mapsto \mathbb{F}_\rho^\#((\Phi^{-1}(\sigma^\#))(\rho))])$. We can then deduce the following theorem:

**Theorem 2 (Relative completeness).** $lfp \mathbb{G}^\# = \Phi([\rho \mapsto lfp \mathbb{F}_\rho^\#])$.

That is to say that applying our analysis on a parametric model, is as precise as applying the initial analysis for each valuation of the Boolean parameters.

# 6 Implementation

Our analysis is integrated within the KaSa static analyzer [3], in the branch named *families-of-models* of the public repository [4]. It is written in OCAML. In this section, we describe the extensions we have done on the frontend to cope with Boolean parameters; then, we explain which data-structures we have used to ensure the scalability of the analysis.

## 6.1 Directives

For the convenience of the modeler, we have extended the frontend to cope with Boolean parameters. Thus, Boolean parameters can be defined, and their values used to condition the application of rules. Also, we have introduced three directives that enable the consideration of some specific hypotheses. These directives are removed and replaced with Boolean parameters at compile time, while the rules are duplicated and refined accordingly. We explain their meaning as follows:

1. The directive *conflict*(*A*, *x*, *y*) specifies that sites *x* and *y* in the occurrences of the protein *A* may be in conflict, that is to say that they cannot be bound in the same occurrence of a protein. This is the situation we have illustrated in our case study. When defined, it is associated with a Boolean predicate $b_i$. The rules that may cause a conflict are detected and duplicated. The classic version remains the same, but it updates its guard *g* to $g \land (\neg b_i)$. The other version is refined by requiring that if *x* or *y* is bound by the rule, the other missing site is defined to be free (the rule is just discarded when it is not possible). The guard *g* of the refined rule is set to $g \land b_i$.
<figure><img src="image_12.png" /><figcaption>Fig. 11. Derivation of two orthogonal sets of patterns for the protein A.</figcaption></figure>

2. The directive sequentialBond(A, x, y) specifies that the site y cannot get bound in an instance of the protein A, when the site x is free (nothing is assumed about potential unbinding rules). It is compiled similarly as the directive conflict(A, x, y).

3. The directive working_set defines the beginning and the end of a section in the model. Within that section, each rule is automatically assigned its own Boolean predicate to represent whether, or not, this rule belongs to the model. This way, the analysis computes which properties depend on which rules, and what the consequences of removing certain rules are.

## 6.2 Binary decision diagrams

The scalability of our implementation heavily relies on the use of binary decision diagrams [6]. In particular, the set of patterns of interest is described as a collection of orthogonal refinements [17]. An orthogonal refinement is a decision tree in which a starting pattern is gradually refined by inserting new information about the potential state of its sites.

*Example 15.* In our case study, the set of patterns of interest (see Fig. 7), is composed of two orthogonal sets of patterns. The orthogonal trees that generated the two sets of patterns are illustrated in Fig. 11. In the first tree, we start with the protein *A* and we list all possible states for the sites *x* and *y* (free and bound). The second tree also starts from the agent *A* and it lists all possible states for *z*. The leaves represent the patterns of interest.

On each leaf of the orthogonal tree, we store the set of boolean valuations under which the corresponding pattern is reachable, in the form of a binary decision diagram. Set operations can be performed symbolically over binary decision diagrams, which improves scalability. Yet, binary decision diagrams may suffer from memory occupancy, as we will discuss in the next section.
<table><caption>**Table 1.** This table compares the runtime of the analysis for different biological models of varying sizes. The size of each biological model is measured in the second column in number of rules and in the third column in number of different biochemical species that may be formed during the model execution (this number is computed by means of static analysis and generative series [11]). In each run, a specific number of rules are added to the working set. This corresponds to the number of boolean predicates that are added to the model for the analysis. The cross (X) indicates a memory overflow.</caption><thead><tr><th rowspan="2">Model</th><th rowspan="2">Nr. Rules</th><th rowspan="2">Nr. Species</th><th colspan="8">Rules in working set</th></tr><tr><th>0</th><th>10</th><th>20</th><th>30</th><th>40</th><th>50</th><th>60</th><th>70</th></tr></thead><tbody><tr><td>EGFR [10]</td><td>20</td><td>932</td><td>0.03s</td><td>0.04s</td><td>0.08s</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>Repressilator</td><td>30</td><td>19</td><td>0.02s</td><td>0.04s</td><td>0.05s</td><td>0.10s</td><td></td><td></td><td></td><td></td></tr><tr><td>FGF</td><td>42</td><td>79080</td><td>0.04s</td><td>0.10s</td><td>0.49s</td><td>1.32s</td><td>2.38s</td><td></td><td></td><td></td></tr><tr><td>SFB [10,25,5]</td><td>65</td><td>~ 10<sup>19</sup></td><td>0.07s.</td><td>0.15s</td><td>0.35s</td><td>0.79s</td><td>1.56s</td><td>4.05s</td><td>19.66s</td><td></td></tr><tr><td>Ensemble [13]</td><td>232</td><td>×</td><td>0.26s</td><td>0.37s</td><td>0.55s</td><td>1.26s</td><td>2.22s</td><td>3.12s</td><td>10.48s</td><td>×</td></tr></tbody></table>

# 7 Experiments

We have tested our prototype [4, branch: families-of-models] on several Kappa models of signaling pathways from the literature, including a small (EGFR) and a large (SFB) model of the integration of the epidermic growth factor, a model of the gLac repressilator (Repressilator), one model (FGF) of integration of the fibroblast growth factor, and one model of protein-protein interactions in yeast (Ensemble). Note that in Ensemble, the number of different biomolecular species cannot be computed due to many kinds of ring formation [13]. The branch in the public repository contains a script to redo these analyses (in the folder `examples/benchmarks/boolean-parameters-CMSB2025`). Our analysis has been done on a MacBook Pro, Apple M1 chip, with 16 GB of memory.

For each model, we introduced *n* Boolean parameters to consider, or ignore, its first *n* rules. The parameter *n* ranges over the values 0, 10, 20, 30, 40, 50, 60, and 70. The analyzer automatically chooses the set of patterns of interest in such a way that it computes the relationships among sites within instances of proteins, relationships between the sites of pairs of agents that may be bound together, and it investigates the formation of double bonds. More details about these properties may be found in [17]. The tool shows, for each rule, under which conditions over the Boolean parameters the tool cannot prove the rule to be unreachable. By Theorem 2, our analysis is as precise as the classical one.

Our analyzer scales well on these parametric models. We were able to complete the analysis of each one with each rule considered as optional, except for the Ensemble model, for which we could consider only 60 rules as optional (which amounts to $2^{60}$ potential instantiations of the model). Memory consumption is the main limiting factor (to store decision diagrams and memoization tables). Such performances have been obtained because the models either include only a few concurrent deep pathways (EGFR, FGF, SFB), or many concurrent ones of small depth (Ensemble). This experiment shows empirically the applicability of our tool on Kappa models of signaling pathways.
## 8 Conclusion

We have formalized, by using the abstract interpretation framework [7,8], a static analysis for parametric models written in Kappa. The analyzer establishes under which conditions over the Boolean parameters of a model, some patterns of interest may be reachable starting from an initial state. Our approach is integrated within the KaSa static analyzer [3], and we were able to show empirically the scalability of our approach on various models of signaling pathways.

This work opens many perspectives. We want to develop static analyses for Meta-modeling languages such as KAMI [21] or iota [22]. These languages let the modeler aggregate knowledge about a model where not all biological assumptions are fully determined yet. Analyzing incomplete models at this level of description would make static analysis available as early as possible in the modeling process. We also would like to exploit the formulation of our analysis by means of Horn clauses to develop an incremental version of this analysis (where rules can be inserted or removed on the fly when editing the model). Lastly, the analysis of parametric models may be useful to study causality in biological models. Indeed, by guarding each rule with a boolean parameter, the analysis computes for each pattern a superset of the boolean parameters that are required for the pattern to be created in the model. As each parameter represents the presence or absence of a rule, the analysis tells us which rules need to be present in order to create the pattern. We want to investigate this connection with causal analysis further.

## References

1. Blinov, M.L., Faeder, J.R., Goldstein, B., Hlavacek, W.S.: Bionetgen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinform. 20(17), 3289-3291 (2004). https://doi.org/10.1093/bioinformatics/bth378

2. Bouguéon, M., Legagneux, V., Hazard, O., Bomo, J., Siegel, A., Feret, J., Théret, N.: A rule-based multiscale model of hepatic stellate cell plasticity: Critical role of the inactivation loop in fibrosis progression. PLoS Comput. Biol. 20(7), 1011858 (2024). https://doi.org/10.1371/journal.pcbi.1011858

3. Boutillier, P., Camporesi, F., Coquet, J., Feret, J., Lý, K.Q., Théret, N., Vognet, P.: Kasa: A static analyzer for kappa. In: Ceska, M., Safránek, D. (eds.) Computational Methods in Systems Biology - 16th International Conference, CMSB 2018, Brno, Czech Republic, September 12-14, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11095, pp. 285-291. Springer (2018). https://doi.org/10.1007/978-3-319-99429-1_17

4. Boutillier, P., Feret, J., Fontana, W., Krivine, J.: Kappa git repository, https://github.com/Kappa-Dev/KappaTools

5. Brightman, F.A., Fell, D.A.: Differential feedback regulation of the mapk cascade underlies the quantitative differences in egf and ngf signalling in pc12 cells. FEBS Letters 482(3), 169-174 (2000). https://doi.org/https://doi.org/10.1016/S0014-5793(00)02037-8

6. Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293-318 (1992). https://doi.org/10.1145/136035.136043; https://doi.org/10.1145/136035.136043
7. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL'77 (1977)

8. Cousot, P., Cousot, R.: Systematic design of program analysis framework. In: Proc. POPL'79 (1979)

9. Danos, V., Feret, J., Fontana, W., Harmer, R., Hayman, J., Krivine, J., Thompson-Walsh, C.D., Winskel, G.: Graphs, rewriting and pathway reconstruction for rule-based models. In: Proc. FSTTCS '12. LIPIcs, vol. 18 (2012)

10. Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Rule-based modelling of cellular signalling. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4703, pp. 17-41. Springer (2007). https://doi.org/10.1007/978-3-540-74407-8_3

11. Danos, V., Feret, J., Fontana, W., Krivine, J.: Abstract interpretation of cellular signalling networks. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings. Lecture Notes in Computer Science, vol. 4905, pp. 83-97. Springer (2008). https://doi.org/10.1007/978-3-540-78163-9_11, https://doi.org/10.1007/978-3-540-78163-9_11

12. Danos, V., Laneve, C.: Formal molecular biology. TCS 325 (1) (2004)

13. Deeds, E.J., Krivine, J., Feret, J., Danos, V., Fontana, W.: Combinatorial complexity and compositional drift in protein interaction networks. PLoS ONE 7 (2012), http://dx.doi.org/10.1371/journal.pone.0032032

14. 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, https://doi.org/10.1016/j.tcs.2008.04.024

15. Feret, J.: Analysis of mobile systems by abstract interpretation. Ph.D. thesis, École Polytechnique, Palaiseau, France (2005), https://tel.archives-ouvertes.fr/pastel-00001303

16. 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比率?file_no=i173

17. Feret, J., Lý, K.Q.: Reachability analysis via orthogonal sets of patterns. In: Sanguinetti, G., Safránek, D. (eds.) Proceedings of SASB 2018, the 7th International Workshop on Static Analysis and Systems Biology, University of Edinburgh, September 7, 2016. Electronic Notes in Theoretical Computer Science, vol. 335, pp. 27-48. Elsevier (2018). https://doi.org/10.1016/J.ENTCS.2018.03.007

18. Folschette, M., Paulevé, L., Magnin, M., Roux, O.F.: Under-approximation of reachability in multivalued asynchronous networks. In: Merelli, E., Troina, A. (eds.) Proceedings of the fourth International Workshop on Interactions between Computer Science and Biology, CS2Bio 2013, Florence, Italy, June 6, 2013. Electronic Notes in Theoretical Computer Science, vol. 299, pp. 33-51. Elsevier (2013). https://doi.org/10.1016/J.ENTCS.2013.11.004, https://doi.org/10.1016/j.entcs.2013.11.004

19. 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
20. Gori, R., Levi, F.: An analysis for proving temporal properties of biological systems. In: Kobayashi, N. (ed.) Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4279, pp. 234–252. Springer (2006). https://doi.org/10.1007/11924661_15, https://doi.org/10.1007/11924661_15

21. Harmer, R., Cornec, Y.L., Légaré, S., Oshurko, E.: Bio-curation for cellular signalling: The KAMI project. IEEE ACM Trans. Comput. Biol. Bioinform. 16(5), 1562–1573 (2019). https://doi.org/10.1109/TCBB.2019.2906164

22. Husson, A., Krivine, J.: A tractable logic for molecular biology. In: Bogaerts, B., Erdem, E., Fodor, P., Formisano, A., Ianni, G., Inclezan, D., Vidal, G., Villanueva, A., Vos, M.D., Yang, F. (eds.) Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, September 20-25, 2019. EPTCS, vol. 306, pp. 101–113 (2019). https://doi.org/10.4204/EPTCS.306.17

23. Kleene, S.C.: Introduction to mathematics. ISHI Press International (1952)

24. 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

25. Schoeberl, B., Eichler-Jonsson, C., Gilles, E.D., Müller, G.: Computational modeling of the dynamics of the map kinase cascade activated by surface and internalized egf receptors. Nature biotechnology 20(4), 370–375 (2002)

26. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2) (1955)

## A Soundness of the Parametric Analysis

In this section, we provide a proof sketch for Theorem 1. We denote as $P \hookrightarrowtail bs$ a pattern $P$ that is contained in the biochemical species $bs$, i.e., there is an embedding from $P$ into $bs$.

Firstly, we show that for each function $\sigma: \mathcal{P} \to \wp(\mathbb{B}^n)$:

$$ \forall P \in \mathcal{P}. ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}](\sigma))(P) \subseteq (\mathbb{G}^{\#}(\sigma))(P) \quad (1) $$

We start by unfolding the definitions of $\Phi$, $\alpha'_{P}$, $\gamma'_{P}$ and $\mathbb{G}$:

$$ \begin{align*} & ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}](\sigma)) \\ &= [\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P}](\rho \mapsto \{P \in \mathcal{P} \mid \rho \in \sigma(P)\}) \\ &= [\Phi \circ \alpha'_{P} \circ \mathbb{G}](\rho \mapsto \{bs \in \mathcal{BS}_{\Sigma} \mid \forall P \in \mathcal{P}. P \hookrightarrowtail bs \Rightarrow \rho \in \sigma(P)\}) \\ &= [\Phi \circ \alpha'_{P}](\rho \mapsto \mathcal{I}_{\rho} \cup \text{Reaction\_prod}) \\ &= \Phi(\rho \mapsto \{P \in \mathcal{P} \mid \exists bs \in (\mathcal{I}_{\rho} \cup \text{Reaction\_prod}) \text{ s.t. } P \hookrightarrowtail bs\}) \\ &= (P \mapsto \{\rho \in \mathbb{B}^n \mid \exists bs \in (\mathcal{I}_{\rho} \cup \text{Reaction\_prod}) \text{ s.t. } P \hookrightarrowtail bs\}). \end{align*} $$

where

$$ \text{Reaction\_prod} = \left\{ bs' \mid \begin{array}{l} \exists R \in \text{Reactions}_{\mathcal{R}_{\rho}} \text{ s.t.} \\ bs' \in \text{Products}(R) \land \\ \forall bs \in \text{Reactants}(R), P \in \mathcal{P}. P \hookrightarrowtail bs \Rightarrow \rho \in \sigma(P) \end{array} \right\} $$
Thus, the set $([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}](\sigma))(P)$ is the set of boolean valuations $\rho \in \mathbb{B}^n$ for which it holds that:

1. either $\exists bs \in \mathcal{I}_{\rho}$ s.t. $P \hookrightarrow bs$, or

2. there exists a species $bs \in \mathcal{BS}_{\Sigma}$ and a reaction $R \in \text{Reactions}_{\mathcal{R}_{\rho}}$, such that:

$$ P \hookrightarrow bs \wedge bs \in \text{Products}(R) \wedge \\ (\forall bs' \in \text{Reactants}(R), P \in \mathcal{P}. \text{ if } P \hookrightarrow bs', \text{ then } \rho \in \sigma(P)). \qquad (2) $$

Let $\rho \in ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}](\sigma))(P)$. It suffices to show for the two cases that $\rho \in (\mathbb{G}^{\#}(\sigma))(P)$.

1. If $\exists bs \in \mathcal{I}_{\rho}$ s.t. $P \hookrightarrow bs$, then there is a boolean formula $g$ such that $(g, bs) \in \mathcal{I}$ and $[[g]]^{\rho} = 1$. Therefore, $\rho \in \text{init}^{\#}(P)$. It follows that $\rho \in (\mathbb{G}^{\#}(\sigma))(P)$.

2. Let $bs \in \mathcal{BS}_{\Sigma}$ and $R : \text{LHS} \rightarrow \text{RHS} \in \text{Reactions}_{\mathcal{R}_{\rho}}$ be the elements for which the properties in Eq. (2) hold. Let $(g, r) \in \mathcal{R}$ be the rule of which $R$ is a refinement, where $r : \text{lhs} \rightarrow \text{rhs}$. As $R \in \text{Reactions}_{\mathcal{R}_{\rho}}$, it means that $[[g]]^{\rho} = 1$. Given that $P \hookrightarrow bs$ and $bs \in \text{RHS}$, there exists an agent in $\text{rhs}$ and an agent in $P$ that are mapped to the same agent in $\text{RHS}$. Thus, we can define the overlap between $\text{rhs}$ and $P$ by merging this agent. We denote the resulting specialized rule as $r' : \text{lhs}' \rightarrow \text{rhs}'$. By refining the $\text{rhs}'$ accordingly, we get the site-graph $\text{RHS}$, therefore $R$ is a refinement of $r'$. This relationship between the three rules $r, r'$ and $R$ is visualized in the Fig. 12. The Horn clauses are built by applying the decision procedure $dp(\text{lhs}')$. We remind the property that holds for the procedure $dp(\text{lhs}')$, that was introduced in Section 5.2:

$$ \forall X^{\#} \subseteq \mathcal{P}, \text{ if } \exists bs \in \gamma_{\mathcal{P}}(X^{\#}) \text{ s.t. } \text{lhs}' \hookrightarrow bs, \\ \text{ then } \exists Cl \in dp(\text{lhs}') \text{ s.t. } Cl \subseteq X^{\#} \qquad (3) $$

In particular, this property holds for $X^{\#} = \alpha_{\mathcal{P}}(\text{Reactants}(R))$. Given that $R$ is a refinement of the rule $r'$, it means that $\text{lhs}' \hookrightarrow \text{bs}''$ for a $\text{bs}'' \in \text{Reactants}(R)$. This implies that $\text{bs}'' \in \gamma_{\mathcal{P}}(\alpha_{\mathcal{P}}(\text{Reactants}(R)))$. Thus, from Eq. (3) we get a clause

$$ \{P_1, \dots, P_k\} \in dp(\text{lhs}') \qquad (4) $$

such that

$$ \{P_1, \dots, P_k\} \subseteq \alpha_{\mathcal{P}}(\text{Reactants}(R)). \qquad (5) $$

Given Eq. (4), it follows that there is a Horn clause $P :=_g P_1, \dots, P_k \in \mathcal{H}_{dp}$. Eq. (5) implies that for each $i \in \{1, \dots, k\}$ it holds that $\exists bs_i \in \text{Reactants}(R)$ such that $P_i \hookrightarrow bs_i$. From this and Eq. (2) it follows that $\forall i \in \{1, \dots, k\}$. $\rho \in \sigma(P_i)$. Therefore, $\rho \in \phi(\sigma, g, \{P_1, \dots, P_k\})$. This concludes the proof of $\rho \in (\mathbb{G}^{\#}(\sigma))(P)$.

We showed that Eq. (1) holds for each abstract state $\sigma$. By induction, we show that:

$$ \forall P \in \mathcal{P}, n \in \mathbb{N}. ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]^n(\sigma))(P) \subseteq ((\mathbb{G}^{\#})^n(\sigma))(P) \qquad (6) $$
<figure><img src="image_13.png" /><figcaption>Fig. 12. Visualization of the relationship between the rule $r:lhs \to rhs$, the refinement $r':lhs' \to rhs'$, the reaction $R:LHS \to RHS$ and the pattern $P$.</figcaption></figure>

For $n = 0$:

$$([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]^{0}(\sigma))(P) = \sigma(P) = ((\mathbb{G}^{\sharp})^{0}(\sigma))(P)$$

We show that $([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]^{n+1}(\sigma))(P) \subseteq ((\mathbb{G}^{\sharp})^{n+1}(\sigma))(P)$, assuming that

$$([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]^{n}(\sigma))(P) \subseteq ((\mathbb{G}^{\sharp})^{n}(\sigma))(P). \quad (7)$$

Given that $[\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]$ is monotonous, it holds that

$$ \begin{align*} & ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]^{n+1}(\sigma))(P) \\ &= ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}][([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]^{n}(\sigma))(P) \\ &\stackrel{(6)}{\subseteq} ([\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]((\mathbb{G}^{\sharp})^{n}(\sigma))(P) \\ &\stackrel{(1)}{\subseteq} (\mathbb{G}^{\sharp}((\mathbb{G}^{\sharp})^{n}(\sigma))(P) \\ &= ((\mathbb{G}^{\sharp})^{n+1}(\sigma))(P). \end{align*} $$

Since $[\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]$ and $\mathbb{G}^{\sharp}$ are continuous, we can apply Kleene iterations [23], which gives

$$\forall P \in \mathcal{P}, (lfp [\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}])(P) \subseteq (lfp \mathbb{G}^{\sharp})(P). \quad (8)$$

As the concretization $\gamma'_{P} \circ \Phi^{-1}$ is monotonic, we have

$$\forall \rho \in \mathbb{B}^n, \gamma'_{P}(\Phi^{-1}((lfp [\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}])))(\rho) \subseteq \gamma'_{P}(\Phi^{-1}((lfp \mathbb{G}^{\sharp} )))(\rho). \quad (9)$$

By [7,8], we have for any Boolean valuation $\rho \in \mathbb{B}^n$:

$$(lfp \mathbb{G})(\rho) \subseteq \gamma'_{P}(\Phi^{-1}(lfp [\Phi \circ \alpha'_{P} \circ \mathbb{G} \circ \gamma'_{P} \circ \Phi^{-1}]))(\rho). \quad (10)$$

Therefore, it holds that for any $\rho \in \mathbb{B}^n$:

$$[lfp \mathbb{G}](\rho) \subseteq \gamma'_{P}(\Phi^{-1}(lfp \mathbb{G}^{\sharp}))(\rho). \quad (11)$$
Applying the definition of $\gamma'_P \circ \Phi^{-1}$ yields:

$$ \gamma'_P(\Phi^{-1}(\text{lfp } \mathbb{G}^{\sharp}))(\rho) = \{bs \in \mathcal{BS}_{\Sigma} \mid \forall P \in \mathcal{P}. P \hookrightarrow bs \Rightarrow \rho \in [\text{lfp } \mathbb{G}^{\sharp}](P)\}. \quad (12) $$

It follows the overall soundness of our analysis: For any pattern of interest $P \in \mathcal{P}$ and any Boolean valuation $\rho \in \mathbb{B}^n$, if there exists a biochemical species $bs \in \mathcal{BS}_{\Sigma}$, such that $P \hookrightarrow bs$ and $bs \in [\text{lfp } \mathbb{G}](\rho)$, then $\rho \in [\text{lfp } \mathbb{G}^{\sharp}](P)$. $\square$

## B Relative Completeness of the Parametric Analysis

This section contains a sketch of the proof for Theorem 2.

We start by showing for each function $\sigma^{\sharp} : \mathcal{P} \to \mathbb{B}^n$ and each pattern $P \in \mathcal{P}$ that

$$ [\mathbb{G}^{\sharp}(\sigma^{\sharp})](P) = [\Phi(\rho \mapsto \mathbb{F}_{\rho}^{\sharp}((\Phi^{-1}(\sigma^{\sharp}))(\rho)))](P). \quad (13) $$

By definition of $\mathbb{G}^{\sharp}$, we get that $[\mathbb{G}^{\sharp}(\sigma^{\sharp})](P)$ is the set of valuations $\rho \in \mathbb{B}^n$ such that:

1. either $\rho \in \text{init}^{\sharp}(P)$, or

2. it holds that:

$$ \rho \in \bigcup_{P := g P_1, \dots, P_k \in \mathcal{H}_{dp}} \phi(\sigma^{\sharp}, g, \{P_1, \dots, P_k\}). \quad (14) $$

We unfold the definitions of $\mathbb{F}_{\rho}^{\sharp}$ and $\Phi$ on the right-hand side of the equality:

$$ \begin{align*} & \Phi(\rho \mapsto \mathbb{F}_{\rho}^{\sharp}((\Phi^{-1}(\sigma^{\sharp}))(\rho))) \\ &= \Phi(\rho \mapsto \mathbb{F}_{\rho}^{\sharp}(\{P \in \mathcal{P} \mid \rho \in \sigma^{\sharp}(P)\})) \\ &= \Phi \left( \rho \mapsto \alpha_{\mathcal{P}}(\mathcal{I}_{\rho}) \cup \left\{ P' \in \mathcal{P} \mid \exists P' := P_1, \dots, P_k \in \mathcal{H}_{dp,\rho} \text{ s.t. } \{P_1, \dots, P_k\} \subseteq \{P \in \mathcal{P} \mid \rho \in \sigma^{\sharp}(P)\} \right\} \right) \\ &= \Phi \left( \rho \mapsto \alpha_{\mathcal{P}}(\mathcal{I}_{\rho}) \cup \left\{ P' \in \mathcal{P} \mid \exists P' := P_1, \dots, P_k \in \mathcal{H}_{dp,\rho} \text{ s.t. } \forall i \in \{1, \dots, k\}. \rho \in \sigma^{\sharp}(P_i) \right\} \right) \\ &= P \mapsto \left\{ \rho \in \mathbb{B}^n \mid \begin{array}{l} P \in \alpha_{\mathcal{P}}(\mathcal{I}_{\rho}) \vee \\ \quad (\exists P := P_1, \dots, P_k \in \mathcal{H}_{dp,\rho} \text{ s.t. } \\ \quad \forall i \in \{1, \dots, k\}. \rho \in \sigma^{\sharp}(P_i)) \end{array} \right\}. \end{align*} $$

The right-hand side of the equality $[\Phi([\rho \mapsto \mathbb{F}_{\rho}^{\sharp}((\Phi^{-1}(\sigma^{\sharp}))(\rho))])(P)$ is the set of valuations $\rho \in \mathbb{B}^n$ for which:

1. either $P \in \alpha_{\mathcal{P}}(\mathcal{I}_{\rho})$, or

2. it holds that:

$$ \exists P := P_1, \dots, P_k \in \mathcal{H}_{dp,\rho} \text{ s.t. } \forall i \in \{1, \dots, k\}. \rho \in \sigma^{\sharp}(P_i). \quad (15) $$

We show that the two first cases $\rho \in \text{init}^{\sharp}(P)$ and $P \in \alpha_{\mathcal{P}}(\mathcal{I}_{\rho})$ are equivalent and that the second case for both sides of the equality are also equivalent.
1. The property $\rho \in \text{init}^{\#}(P)$ holds iff: $\exists (g, bs) \in \mathcal{I}$ such that $P \hookrightarrowtail bs$ and $[[g]]^\rho = 1$. This holds iff $P \in \alpha_P(\mathcal{I}_\rho)$.

2. A Horn clause $P := P_1, \dots, P_k \in \mathcal{H}_{dp,\rho}$ iff $P :=_g P_1, \dots, P_k \in \mathcal{H}_{dp}$ and $[[g]]^\rho = 1$. From this and the definition of $\phi$ we derive that the Eqs. (14) and (15) are equivalent.

This proves the equality shown in Eq. (13).

We show by induction that

$$ (\mathbb{G}^{\#})^{n}(\sigma^{\#}) = \Phi(\rho \mapsto (\mathbb{F}_{\rho}^{\#})^{n}((\Phi^{-1}(\sigma^{\#}))(\rho))) \quad (16) $$

For $n = 0$:

$$ \begin{aligned} \Phi(\rho \mapsto (\Phi^{-1}(\sigma^{\#}))(\rho)) &= \Phi(\rho \mapsto \{P \in \mathcal{P} \mid \rho \in \sigma^{\#}(P)\}) \\ &= (P \mapsto \{\rho \in \mathbb{B}^n \mid \rho \in \sigma^{\#}(P)\}) = \sigma^{\#} \end{aligned} $$

Then we prove $(\mathbb{G}^{\#})^{n+1}(\sigma^{\#}) = \Phi(\rho \mapsto (\mathbb{F}_{\rho}^{\#})^{n+1}((\Phi^{-1}(\sigma^{\#}))(\rho)))$, assuming that

$$ (\mathbb{G}^{\#})^{n}(\sigma^{\#}) = \Phi(\rho \mapsto (\mathbb{F}_{\rho}^{\#})^{n}((\Phi^{-1}(\sigma^{\#}))(\rho))) \quad (17) $$

It holds that

$$ \begin{aligned} & (\mathbb{G}^{\#})^{n+1}(\sigma^{\#}) \\ &= \mathbb{G}^{\#}((\mathbb{G}^{\#})^{n}(\sigma^{\#})) \\ \stackrel{(17)}{=} & \mathbb{G}^{\#}(\Phi(\rho \mapsto (\mathbb{F}_{\rho}^{\#})^{n}((\Phi^{-1}(\sigma^{\#}))(\rho)))) \\ \stackrel{(13)}{=} & \Phi(\rho \mapsto \mathbb{F}_{\rho}^{\#}((\Phi^{-1}(\Phi(\rho \mapsto (\mathbb{F}_{\rho}^{\#})^{n}((\Phi^{-1}(\sigma^{\#}))(\rho)))))(\rho))) \\ &= \Phi(\rho \mapsto \mathbb{F}_{\rho}^{\#}((\mathbb{F}_{\rho}^{\#})^{n}((\Phi^{-1}(\sigma^{\#}))(\rho)))) \\ &= \Phi(\rho \mapsto (\mathbb{F}_{\rho}^{\#})^{n+1}((\Phi^{-1}(\sigma^{\#}))(\rho))). \end{aligned} $$

Since $\mathbb{G}^{\#}$ and $\mathbb{F}_{\rho}^{\#}$ are continuous, we can apply Kleene iterations [23], which gives

$$ lfp \mathbb{G}^{\#} = \Phi([\rho \mapsto lfp \mathbb{F}_{\rho}^{\#}]). \quad (18) $$

□