Incremental KaSa: Static Analysis of Kappa Models at Edit Time (supplementary resources)

This website provides some supplementary resources about the following paper:

Incremental Kasa: Static Analysis of Kappa Models at Edit Time

which has been accepted as a tool paper at CMSB 2026.

@InProceedings{feret:CMSB2026b,
  title = "Incremental KaSa: Static Analysis of Kappa Models at Edit Time.",
  booktitle = "Twenty fourth  International Workshop on Static Analysis and Systems Biology (SASB'26)",
  series = "LNCS/LNBI",
  publisher = "springer",
  volume = "????",
  pages = "??-??"
  note = "to appear, Supplementary information available at \url{www.di.ens.fr/~feret/Incremental-KaSa-tool-paper}",
  author = "Rebecca Ghuidini and J{\'e}r{\^o}me Feret"}

Kappa

Electron application

The tool is available as an electron app under various operating systems.

• Linux
• MacOS
• Windows

Installation from the sources

Sources may be downloaded on the github repository in the branch incremental-KaSa (we plan to merge it into master for version 5.0).

git clone https://github.com/Kappa-Dev/KappaTools.git
cd KappaTools  
git checkout incremental-KaSa

The file README.md contains all the information to compile the tools and to run the benchmarks.

Kappa handbook

Kappa handbook may be found here.

Examples of the paper

• Use case: wrong_model.ka correct_model.ka
• TGF V19: NTactivationTGF_19.ka
• TGF 20180419: NTactivationTGF_20180419.ka
• WNT 20151228: bigwnt_20151228.ka
• WNT_20170322: bigwnt_20170322.ka
• KORKUT 20170113: korkut_20170113.ka
• KORKUT 20170206: korkut_20170206.ka

Use case

Description

We illustrate a typical usage of our incremental analyzer: A modeler is revising a part of a larger model that describes the behavior of some membrane receptors.

Two types of protein are concerned:

Ligand instances (EGF) will be colored blue circles and receptor instances (EGFR) green hexagons. Each instance of receptor has four binding sites, one in white to connect with ligand instances, one in blue to bind at the same site of other receptor instances, and the third one in yellow to bind to the fourth one in pink of other receptor instances.

We now describe the binding rules:
• Ligand instances bind to the receptor instances to activate them.
  

  EGF(r[.]),EGFR(l[.]) -> EGF(r[1]),EGFR(l[1])

• The activated receptor instances then pairwise bind with a symmetric bond.
  

  EGFR(l[_],r[.]),EGFR(l[_],r[.]) -> EGFR(l[_],r[1]),EGFR(r[_],l[1])

• Lastly, a non-symmetric bond is formed to distinguish the role of the two receptor instances in dimer instances.
  

  EGFR(r[_],c[.]),EGFR(r[_],n[.]) -> EGFR(r[_],c[1]),EGFR(r[_],n[1])

A key property in this model part is that it is impossible to chain three receptor instances. The modeler introduces a fictitious rule as follows:

EGFR(r[1]),EGFR(r[1],c[2]),EGFR(n[2]) -> EGFR(r[1]),EGFR(r[1],c[2]),EGFR(n[2])

to assess this property. He expects the analyzer to detect that this fictitious rule can never be applied, which is true.

The modeler then considers rules to break the links between protein instances.

• A ligand instance disconnects from a receptor instance when the blue site of the latter is free.
  

  EGF(r[1]),EGFR(l[1]) -> EGF(r[.]),EGFR(l[.])

• All other sites in receptor instances may be freed without conditions.
  

  EGFR(r[1]),EGFR(r[1]) -> EGFR(r[.]),EGFR(r[.])

  

  EGFR(c[1]),EGFR(n[1]) -> EGFR(c[.]),EGFR(n[.])

Unfortunately, with these new rules, the fictitious rule is no longer detected to be unreachable. Thus, either the analysis is not precise enough (due to the abstraction), or the property of interest is not satisfied anymore.

The modeler uses the incremental analyzer to check the result of the analysis when one of the four unbinding rules is discarded. In this way, the property of interest is recovered when the second rule is discarded.

The modeler replaces it with the following one:

EGFR(r[1],c[.],n[.]),EGFR(r[1],c[.],n[.]) -> EGFR(r[.],c[.],n[.]),EGFR(r[.],c[.],n[.])

The reader is still alerted that the fictitious rule is unreachable. This proves that the expected property is satisfied in the (corrected) model.

Now we provide both versions of the model:

• Wrong model.
• Corrected model

Launch the KaSa agent with the wrong model:

./bin/KaSaIncremental --current-chapter examples/incremental_analysis/use_case/wrong_model.ka

Then at prompt type the following instruction:

update file examples/incremental_analysis/use_case/correct_model.ka as examples/incremental_analysis/use_case/wrong_model.ka

or copy paste the following models:

in the user interface.

Quick start

Use the GUI

To test the GUI, open the file examples/incremental_analysis/simple_example.kawith the button File -> Open.

This model contains four agent types: A, B, C and D. The initial state contains the agents D and B. The agent A can be created by the rule 'create.A.if.D', if an agent D is present. The contact map shows the four types of agents. If the "high accuracy" contact map is chosen, we see that the agent C can never be formed. To solve this, we can add the initial state:

%init: 100 C(c{u})

If we do that, the analysis is updated incrementally and the warning "dead agent" disappears.

By disabling the checkboxes in front of the rules or initial states, we can see how the result of the analysis changes when some rules are removed. For example, when disabling the rule 'bind.A_A', the model cannot form any unbounded polymers anymore. And when disabling the first initial state of the agent D, the agents D and A become unreachable.

Use the Interactive CLI

Note: for windows, use the command

.\_build\install\default\bin\KaSaIncremental.exe

instead of

./bin/KaSaIncremental

.

The CLI can be lauched with an example model by running:

./bin/KaSaIncremental --current-chapter examples/incremental_analysis/simple_example.ka 

The analysis prints the constraints that were calculated by the reachability analysis. For example, it says that C cannot occur in the model. This can be fixed by adding the inital state:

%init: 100 C(c{u}) in the file examples/incremental_analysis/simple_example.ka

and updating the analysis.

The analysis can be updated by typing:

update file examples/incremental_analysis/simple_example.ka

in the interactive agent. After this, the analysis says "all agents may occur in the model". Rules can be disabled by their label, for example:

disable 'create.A.if.D'

Subsequently, they can be enabled again:

enable 'create.A.if.D'

The command help prints more information about available commands.

Change log

Since the submission of the paper (2026/04/11), we have made the following contributions to the tool:

• Expressivity: We improved the reduced product, which communicate properties from the abstract domains to the others.
• Performance: Although the computation of the analysis fixpoint is done incrementally, data-strutures are computed in the preprocessing phase to schedule the order of the rule applications. We have modified the setting of this data-structures to make some parts of it incremental as well.
• Ergonomy: We have improved the graphical user-interdace;

Benchmarks

Core benchmarks

Use the scripts

You may launch the scripts from the root of the repository by prompting the following instructions:
Warning the second script takes about 8 hours on an apple M4 Max chip.

git clone https://github.com/Kappa-Dev/KappaTools.git
cd KappaTools
git checkout incremental-KaSa
./examples/benchmarks/incremental-KaSa/script_disable_and_add_rules -i
./examples/benchmarks/incremental-KaSa/script_compare_working_set_size -i

(When the -i option is used, the tools are built automatically with all the dependencies.)

Kappa models

• TGF V19: NTactivationTGF_19.ka
• TGF 20180419: NTactivationTGF_20180419.ka
• WNT 20151228: bigwnt_20151228.ka
• WNT_20170322: bigwnt_20170322.ka
• KORKUT 20170113: korkut_20170113.ka
• KORKUT 20170206: korkut_20170206.ka

Tables and plots

Extended benchmarks

Use the scripts with the option -e.

You may launch the scripts from the root of the repository by prompting the following instructions:
Warning the second script takes about X hours on an apple M4 Max chip.

git clone https://github.com/Kappa-Dev/KappaTools.git
cd KappaTools
git checkout incremental-KaSa
opam install . --update-invariant --deps-only
dune build
make all
./examples/benchmarks/incremental-KaSa/script_disable_and_add_rules -e 
./examples/benchmarks/incremental-KaSa/script_compare_working_set_size -e 

Kappa models

• FGF: fgf.ka
• EGF: egf.ka
• YEAST (ensemble): ensemble.ka
• YEAST (machine): machine.ka
• TGF V19: NTactivationTGF_19.ka
• TGF V20: NTactivationTGF_20.ka
• TGF V21: NTactivationTGF_21.ka
• TGF 20170401: NTactivationTGF_20170401.ka
• TGF 20180419: NTactivationTGF_20180419.ka
• WNT 20151228: bigwnt_20151228.ka
• WNT_20160928: bigwnt_20160928.ka
• WNT_20170322: bigwnt_20170322.ka
• KORKUT 20170113: korkut_20170113.ka
• KORKUT 20170117: korkut_20170117.ka
• KORKUT 20170206: korkut_20170206.ka

Tables and plots

References

Models

1. William Hlavacek, James Faeder, Michael Blinov, Richard Posner, Michael Hucka, & Walter Fontana: Rules for Modeling Signal-Transduction Systems. Science’s STKE 2006. 344 (2006)

3. Frances Brightman & David Fell: >Differential feedback regulation of the MAPK cascade underlies the quantitative differences in EGF and NGF signalling in PC12 cells. FEBS Lett. 482(3), 169–174 (2000)

4. Birgit Schoeberl, Claudia Eichler-Jonsson, Ernst Gilles, & Gertraud Müller: Computational modeling of the dynamics of the map kinase cascade activated by surface and internalized EGF receptors. Nature Biotechnology 20, 370–375 (2002)

6. Eric J. Deeds, Jean Krivine, Jérôme Feret, Vincent Danos,& Walter Fontana. Combinatorial complexity and compositional drift in protein interaction networks. In PLoS ONE, volume 7(3). © 2012, Public Library of Science.

7. Benjamin Gyori, John Bachman, Kartik Subramanian, Jeremy Muhlich, Lucian Galescu et Peter Sorger. From word models to executable models of signaling networks using automated assembly. Molecular Systems Biology, 13, 2017.

Tools

1. Boutillier, P., Feret, J., Krivine, J., Q., Kim Ly: Kasim development homepage, http://kappalanguage.org.

2. Pierre Boutillier, Ferdinanda Camporesi, Jean Coquet, Jérôme Feret, Kim Quyên Lý, Nathalie Theret, & Pierre Vignet. KaSa: A Static Analyzer for Kappa In Computational Method in Systems Biology, tools paper track (CMSB 2018), In: Lecture Notes in Computer Sciences / Lecture Notes in BioInformatics, volume 11095. © 2018, Springer.

3. Pierre Boutillier, Mutaamba Maasha, Xing Li, Héctor F. Medina-Abarca, Jean Krivine, Jérôme Feret, Ioana Cristescu, Angus G. Forbes, & Walter Fontana. The Kappa platform for rule-based modeling. In: Bioinformatics, Volume 34(13). © 2018. Oxford Academic.

Theory

1. Jérôme Feret and Rebecca Ghidini. Reachability Analysis for Parametric Rule-Based Models. In Computational Method in Systems Biology, (CMSB 2025), In: Lecture Notes in Computer Sciences / Lecture Notes in BioInformatics, volume 15959, pp 153--173. © 2025, Springer.

2. Jérôme Feret & Kim Quyên Lý. Reachability analysis via orthogonal sets of patterns. In the PostProceedings of the 7th International Workshop on Static Analysis and Systems Biology (SASB 2016). In Electronic Notes in Theoretical Computer Science, volume 335. © 2018, Elsevier Science.

3. Vincent Danos, Jérôme Feret, Walter Fontana,& Jean Krivine. Abstract interpretation of cellular signalling networks. In Verification, Model Checking, and Abstract Interpretation, VMCAI 2008, number 4905 in Lecture Notes in Computer Sciences. 2008. © Springer.