The ODEs are given from line 204 to line 228:

We now wonder whether the sites are equivalent or not. We use the following command line:

KaDE --rule-rate-convention Biochemist sym.ka --show-symmetries

The status of equivalent sites is described in the log:

The set of rules and the initial state are symmetric with respect to the pair of sites. This is not the case of the observable. Thus, only backward bisimulation may be used to reduce the system. Indeed, if we ignore the difference between sites x and y, we can no longer express the concentration of the sites x that are free. This excludes forward bisimulation. Backward bisimulations may still be used since the concentration of each species can be computed by from the overall concentration of its equivalence class, since the concentration of two equivalent species are always inversely proportional to their number of automorphisms.

The command line:

 KaDE --rule-rate-convention Biochemist sym.ka --with-symmetries Forward --output ode_with_fwd_sym --output-plot data_fwd.csv

give this octave file. There is indeed no reduction. This is because we observe the concentration of asymetric dimers (where a site x is bound to a site y). Forward bisimulation would ignore the difference between symmetric and asymmetric dimers.

The command line:

 KaDE --rule-rate-convention Biochemist sym.ka --with-symmetries Backward --output ode_with_bwd_sym --output-plot data_bwd.csv

reduces the system by ignoring the difference between sites x and y. This is done by replacing in each product of reaction, every species by an arbitrary representative of its equivalence class, and in each algebraic expression, each species concentration by the product between the concentration of its representative and the relative weight of this species in its equivalence class (which is constant and inversely proportional to its number of automorphisms.)

The OCTAVE output is this file. We notice at line 29, that only three variables remain:

The meaning of these variables is given from line 173 to line 182:

Thus, there is one variable for time advance, one for free As, and one for dimers. The three kinds of dimers are gathered into a single equivalence class (no matter which sites are bound). KaDE has gathered the three kinds of dimers into a single equivalence class (no matter with sites are bound). For instance, from line $211$ to line $212$:

the production of an asymmetric dimer, is replaced with the production of a dimer in which the bond is on both sites y.

The definition of observables is given from line $289$ to line $301$:

We are interested in asymetric dimers only. We notice that their concentration is obtained by dividing the overall quantity of dimers by $4$. To understand why, we shall have a closer look at the meaning of each variable. There exist two conventions. One variable may denote the number of occurrences of a bio-molecular species, or the number of embeddings between this bio-molecular species and the current state of the system. Both conventions are related by the fact, that the number of embeddings is equal to the number of occurrences multiplied by the number of automorphisms in the bio-molecular species. The reduction of the model replace each occurrence of a dimer into a dimer made of two proteins bond via their site y.

As indicated at line 15:

the convention is to count in number of embeddings. Thus the total number of dimers is $y\left(2\right)$/$2$. Then half of them only is an asymetric dimer, which gives $y\left(2\right)$/$4$

SBML2LaTeX may be used to convert the output of KaDE into PDF.

Firstly, we translate the different versions of the models in SBML.

KaDE sym.ka --ode-backend SBML --output network
KaDE sym.ka --ode-backend SBML --output network_fwd --with-symmetries Forward
KaDE sym.ka --ode-backend SBML --output network_bwd --with-symmetries Backward

The following command line:

java -jar

launches the graphical interface of SBML2LaTeX.

We compile the LaTeX files thanks to the following instructions:

pdflatex network.tex
pdflatex network.tex
pdflatex network_fwd.tex
pdflatex network_fwd.tex
pdflatex network_bwd.tex
pdflatex network_bwd.tex

Let us check the soundness of our tools, by integrating both ODEs systems.

octave ode.m
octave ode_fwd.m
octave ode_bwd.m

We obtain the three following files: data.csv -- data_fwd.csv -- data_bwd.csv.

The concentration of asymetric dimers may be plotted thanks to gnuplot. We use the following gnuplot files: plot.gplot -- plot_fwd.gplot -- plot_bwd.gplot.

gnuplot plot.gplot
gnuplot plot_fwd.gplot
gnuplot plot_bwd.gplot

We obtain the following plots:

Parametric examples

The paper consider three examples, with a parametric size, that we denote by n. We give the Kappa files for each of the three examples with parameter n = 2.

kinase/phosphatase

multiple phosphorylation sites

multiple phosphorylation sites with counter

All the files for the description of the models, both in Kappa and in BNGL may be found in this tarball.

All the files, including both the input models and the reduced ones, may be found in this tarball.

kinase/phosphatase

Building Kappa and BNGL models

Here is an OCaml source code to generate the model.
The following instructions:

ocamlopt.opt kinase_phosphatase.ml  -o kinase_phosphatase
mkdir generated_models
mkdir generated_models/kin_phos
./kinase_phosphatase 1 10 

ls generated_models/kin_phos

The Kappa model matches with the BNGL model with distinct sites.

Tarball

Input/output files

Benchmarks

Each computation has been made with a 10 minutes time-out. Computations have been made on a MacBookPro with a 2.8 GHz Intel Core i7 CPU and a 16 Go 1600 MHz DDR3 memory.

In particular we propose to compare the computation of several pipelines for several functionnalities.

1. Firstly, we compare the computation to generate the ground network with BNGL and with KaDE. We obtain the following plots:



2. Secondly, we compare the computation to generate the network reduced by forward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NFB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to prove the optimality. In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of forward bisimulation (using the faster, but potentially incomplete, algorithm FB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL. ERODE can also go further by inferring the coarsest bisimulation that is specified by a parition of the set of bio-molecular species.
   
   We obtain the following plots:



3. Thirdly, we compare the computation to generate the network reduced by backward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NBB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to search for further potential reduction (since ERODE focuses on uniform bisimulation, it cannot prove the optimality of the reduction). In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of backward bisimulation (using the faster, but potentially incomplete, algorithm BB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL.
   
   We obtain the following plots:

multi-phosphorilation sites

Building Kappa and BNGL models

Here is an OCaml source code to generate the model.

The following instructions:

ocamlopt.opt kinase_phosphatase.ml  -o kinase_phosphatase
mkdir generated_models
mkdir generated_models/kin_phos
./multi_phos 1 10 

ls generated_models/multi_phos

The Kappa model matches with the BNGL model with distinct sites.

Tarball

Input/output files

Benchmarks

Each computation has been made with a 10 minutes time-out. Computations have been made on a MacBookPro with a 2.8 GHz Intel Core i7 CPU and a 16 Go 1600 MHz DDR3 memory.

In particular we propose to compare the computation of several pipelines for several functionnalities.

1. Firstly, we compare the computation to generate the ground network with BNGL and with KaDE. We obtain the following plots:



2. Secondly, we compare the computation to generate the network reduced by forward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NFB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to prove the optimality. In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of forward bisimulation (using the faster, but potentially incomplete, algorithm FB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL. ERODE can also go further by inferring the coarsest bisimulation that is specified by a parition of the set of bio-molecular species.
   
   We obtain the following plots:



3. Thirdly, we compare the computation to generate the network reduced by backward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NBB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to search for further potential reduction (since ERODE focuses on uniform bisimulation, it cannot prove the optimality of the reduction). In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of backward bisimulation (using the faster, but potentially incomplete, algorithm BB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL.
   
   We obtain the following plots:

multi-phosphorilation sites (encoded with explicit counter)

Building Kappa and BNGL models

Here is an OCaml source code to generate the model.

The following instructions:

ocamlopt.opt multi_phos_with_counter.ml  -o multi_phos_with_counter
mkdir generated_models
mkdir generated_models/multi_phos_with_counter
./multi_phos_with_counter 1 10 

ls generated_models/multi_phos_with_counter

The Kappa model matches with the BNGL model with distinct sites.

Tarball

Input/output files

Benchmarks

Each computation has been made with a 10 minutes time-out. Computations have been made on a MacBookPro with a 2.8 GHz Intel Core i7 CPU and a 16 Go 1600 MHz DDR3 memory.

1. Firstly, we compare the computation to generate the ground network with BNGL and with KaDE. We obtain the following plots:



2. Secondly, we compare the computation to generate the network reduced by forward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NFB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to prove the optimality. In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of forward bisimulation (using the faster, but potentially incomplete, algorithm FB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL. ERODE can also go further by inferring the coarsest bisimulation that is specified by a parition of the set of bio-molecular species.
   
   We obtain the following plots:



3. Thirdly, we compare the computation to generate the network reduced by backward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NBB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to search for further potential reduction (since ERODE focuses on uniform bisimulation, it cannot prove the optimality of the reduction). In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of backward bisimulation (using the faster, but potentially incomplete, algorithm BB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL.
   We obtain the following plots:

Other examples

We have manually translated each model of the BNGL distribution into Kappa. We have used the static analyzer KaSa to check that there is no dead code in models. We found the rule for transphosphorylation of Fyn by SH2-bound Lyn was wrong in each BNGL model, we corrected it as well as in the kappa models.

Remark on equivalent sites

It is worth noticing that the operational semantics on equivalent sites in BNGL does not match with the intuitive encoding with multiple identified sites. Let us consider an example with a protein A with a site x that may take the state u or p and two sites l that may take the state u, p, or q.

We consider the following rule in BNGL:

This means that the site x of a protein A may get the state p at rate k provided that at least one site l is in state u.

An intuitive encoding with identified sites would be the following:

The previous encoding is quantitatively wrong, both rules may be used to activate the site x of a protein A with both sites l1 and l2 in state u, with an overall rate of 2k (instead of k in the BNGL model with equivalent sites).

This approach can be generalised. Consider a protein with some equivalent sites. Consider a rule that tests some of these sites. For each occurrence of agent and each kind of equivalent sites, the sites of this kind may be partitioned into isomorphic classes (two distinct classes stand for two distinct properties to specify the context of the site). Let us assume that there are n equivalence classes. Then we have to consider every function mapping each of the equivalent sites to a subset of these equivalence classes. The interpretation of each function is that each site matches the context of (or the property denoted by) each equivalence class in its image. Then each function is associated with a set of rules. The rule is obtained by refining the initial ones by enforcing, for each site, the properties to be satisfied (for each equivalence class in the image of the site), and enforcing the negation of the properties that are not (for each equivalence class that is not in the image of the site). Since there is no negation, enforcing the negation of a property requires to cover all the other cases, by a set of mutually incompatible conditions.

Some conditions (positive and/or negative) may not be compatible. Thus, a solver may be used to cut irrealisable refinements on the fly.

Input files

This table contains the examples that are provided in the BNGL repository. For each model, we provide the BNGL file and the Kappa model.

Benchmarks

Each computation has been made with a 10 minutes time-out. Computations have been made on a MacBookPro with a 2.8 GHz Intel Core i7 CPU and a 16 Go 1600 MHz DDR3 memory.

In particular we propose to compare the computation of several pipelines for several functionnalities.

1. Firstly, we compare the computation to generate the ground network with BNGL and with KaDE. We obtain the following plots:



2. Secondly, we compare the computation to generate the network reduced by forward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction. In the second pipeline, we skip the proof of optimality. In the third pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to prove the optimality. In the fourth pipeline, we skip the proof of optimality. In the fifth pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of forward bisimulation.
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL. ERODE can also go further by inferring the coarsest bisimulation that is specified by a parition of the set of bio-molecular species.
   
   We obtain the following plots:



3. Thirdly, we compare the computation to generate the network reduced by backward bisimulation. In the first pipeline, we use KaDE to generate a reduced network, then we use ERODE to prove the optimality of the reduction (using the algorithm NBB). In the second pipeline, we specify explicitely in the BNGL model, which sites are equivalent, we use BNGL to generate the reduced model, and then we use ERODE to search for further potential reduction (since ERODE focuses on uniform bisimulation, it cannot prove the optimality of the reduction). In the third pipeline, we use BNGL to generate the ground network, and then we use ERODE to reduce this network by the means of backward bisimulation (using the faster, but potentially incomplete, algorithm BB).
   
   It is worth stressing out that equivalent sites are infered automatically by KaDE and ERODE, whereas they have to be specified explicitly by the end-used in BNGL.
   
   We obtain the following plots:

References

1. Boutillier, P., Feret, J., Krivine, J., Q., Kim Ly: Kasim development homepage, http://kappalanguage.org.
2. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: ERODE: A tool for the evaluation and reduction of ordinary differential equations. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II. pp. 310--328 (2017)
3. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: ERODE website. http://sysma.imtlucca.it/tools/erode/
4. Draeger, A., Planatscher, H., Wouamba, D.M., Schroder, A., Hucka, M., Endler, L., Golebiewski, M., Muller, W., Zell, A.: SBML2LATEX: Conversion of SBML files into human-readable reports. Bioinformatics 25(11), 1455--1456 (Apr 2009) http://www.cogsys.cs.uni-tuebingen.de/software/SBML2LaTeX/
5. Eaton, J.W., Bateman, D., Hauberg, S., Wehbring, R.: GNU Octave version 4.0.0 manual: a high-level interactive language for numerical computations. Free Software Foundation (2015), http://www.gnu.org/software/octave/doc/~interpreter
6. Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: Rule-based modeling of biochemical systems with bionetgen. Methods Mol Biol 500, 113--67 (2009)
7. Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: BioNetGen Distributions. http://bionetgen.org/index.php/BioNetGen_Distributions.
8. Funahashi, A., Matsuoka, Y., Jouraku, A., Morohashi, M., Kikuchi, N., Kitano, H.: Celldesigner 3.5: A versatile modeling tool for biochemical networks. Proceedings of the IEEE 96 (2008). http://www.celldesigner.org
9. Hucka, M., Bergmann, F.T., Hoops, S., Keating, S.M., Sahle, S., Schaff, J.C., Smith, L.P., Wilkinson, D.J.: The systems biology markup language (sbml): Language specification for level 3 version 1 core (2010). http://www.cogsys.cs.uni-tuebingen.de/software/SBML2LaTeX/
10. MATLAB: version 9.2. The MathWorks Inc., Natick, Massachusetts (2017). https://fr.mathworks.com/products/matlab.html
11. Monagan, M.B., Geddes, K.O., Heal, K.M., Labahn, G., Vorkoetter, S.M., Mc-Carron, J., DeMarco, P.: Maple 10 Programming Guide. Maplesoft, Waterloo ON, Canada (2005). http://www.maplesoft.com/solutions/education/
12. Wolfram Research, I.: Mathematica. Wolfram Research, Inc. (2017). https://www.wolfram.com/mathematica/

1. Camporesi, F., Feret, J.: Formal reduction for rule-based models. Electronic Notes in Theoretical Computer Science 276, 29 -- 59 (2011), sciencedirect link.
2. Camporesi, F., Feret, J., Koeppl, H., Petrov, T.: Combining model reductions. Electronic Notes in Theoretical Computer Science 265, 73 -- 96 (2010), sciencedirect link.
3. Feret, J.: An algebraic approach for inferring and using symmetries in rule-based models. Electronic Notes in Theoretical Computer Science 316, 45 -- 65 (2015), 5th International Workshop on Static Analysis and Systems Biology (SASB 2014)
4. Feret, J., Koeppl, H., Petrov, T.: Stochastic fragments: A framework for the exact reduction of the stochastic semantics of rule-based models. International Journal of Software and Informatics 7(4), 527 -- 604 (2013)