Proving Unreachability in Automata Networks by Mixing Static Analysis and Bounded Model Checking - l'unam - université nantes angers le mans Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2023

Proving Unreachability in Automata Networks by Mixing Static Analysis and Bounded Model Checking

Résumé

Discrete models have been widely used in the field of bioinformatics, more especially in Systems Biology. Automata Network is a powerful modeling framework which can represent different dynamics on complex systems. The study of its dynamical properties has multiple purposes. Among these properties, reachability is of crucial interest for many real life applications (e.g. in biological regulatory networks). For example, it can give interesting insights about the behavior of the biological system. Additionally, it can be used to validate a model regarding the biological literature. In the last decade, some approaches have been shown of interest to address instances with hundreds of components. They are based on approximations that however lead to non-conclusiveness on some examples that may appear in practical biological examples. In this work, we present an approach combining static analysis with Bounded Model Checking to decide about the unreachable case. The originality of our method lies in the computation of a sufficient bound on the length of execution sequences, derived from previous works using static analysis.
Fichier principal
Vignette du fichier
paper.pdf (518.38 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03959546 , version 1 (01-02-2023)

Identifiants

  • HAL Id : hal-03959546 , version 1

Citer

Samuel Buchet, Morgan Magnin, Olivier Roux. Proving Unreachability in Automata Networks by Mixing Static Analysis and Bounded Model Checking. 2023. ⟨hal-03959546⟩
31 Consultations
31 Téléchargements

Partager

Gmail Facebook X LinkedIn More