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 de l'École normale supérieure, 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).
Type de document :
Communication dans un congrès
David Safranek; Guido Sanguinetti. 7th International Workshop on Static Analysis and Systems Biology, (SASB 2016), Sep 2016, Edinburgh, United Kingdom. Elsevier, ENTCS, Static Analysis and Systems Biology. 〈http://sasb2016.fi.muni.cz〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01379902
Contributeur : Jérôme Feret <>
Soumis le : mardi 15 novembre 2016 - 09:43:59
Dernière modification le : jeudi 26 avril 2018 - 10:29:01
Document(s) archivé(s) le : mercredi 15 mars 2017 - 04:27:20

Fichier

orthogonal_patterns.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01379902, version 1

Collections

Citation

Jérôme Feret, Kim Quyen Ly. Reachability analysis via orthogonal sets of patterns. David Safranek; Guido Sanguinetti. 7th International Workshop on Static Analysis and Systems Biology, (SASB 2016), Sep 2016, Edinburgh, United Kingdom. Elsevier, ENTCS, Static Analysis and Systems Biology. 〈http://sasb2016.fi.muni.cz〉. 〈hal-01379902〉

Partager

Métriques

Consultations de la notice

326

Téléchargements de fichiers

66