Skip to Main content Skip to Navigation
Conference papers

Reachability analysis via orthogonal sets of patterns

Jérôme Feret 1 Kim Quyen Ly 1 
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique - ENS Paris, Inria de Paris
Abstract : Rule-based modelling languages, such as Kappa, allow for the description of very detailed mechanistic models. Yet, as the rules become more and more numerous, there is a need for formal methods to enhance the level of confidence in the models that are described with these languages. We develop abstract interpretation tools to capture invariants about the biochemical structure of the bio-molecular species that may occur in a given model. In previous works, we have focused on the relationships between the states of the sites that belong to the same instance of a protein. This comes down to detect for a specific set of patterns, which ones may be reachable during the execution of the model. In this paper, we generalise this approach to a broader family of abstract domains that we call orthogonal sets of patterns. More precisely, an orthogonal set of patterns is obtained by refining recursively the information about some patterns containing a given protein, so as to partition the set of occurrences of this protein in any mixture. We show that orthogonal sets of patterns offer a convenient choice to design scalable and accurate static analyses. As an example, we use them to infer properties in models with transport of molecules (more precisely, we show that each pair of proteins that are connected, always belong to the same compartment), and models involving double bindings (we show that whenever a protein of type A is bound twice to proteins of type B, then the protein A is necessarily bound twice to the same instance of the protein B).
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Jérôme Feret Connect in order to contact the contributor
Submitted on : Tuesday, November 15, 2016 - 9:43:59 AM
Last modification on : Wednesday, June 8, 2022 - 12:50:03 PM
Long-term archiving on: : Wednesday, March 15, 2017 - 4:27:20 AM


Files produced by the author(s)


  • HAL Id : hal-01379902, version 1



Jérôme Feret, Kim Quyen Ly. Reachability analysis via orthogonal sets of patterns. 7th International Workshop on Static Analysis and Systems Biology, (SASB 2016), David Safranek; Guido Sanguinetti, Sep 2016, Edinburgh, United Kingdom. ⟨hal-01379902⟩



Record views


Files downloads