Exact Boolean Abstraction of Linear Equation ...
Type de document :
Compte-rendu et recension critique d'ouvrage
Titre :
Exact Boolean Abstraction of Linear Equation Systems
Auteur(s) :
Allart, Emilie [Auteur]
BioComputing
Niehren, Joachim [Auteur]
BioComputing
Linking Dynamic Data [LINKS]
Versari, Cristian [Auteur]
BioComputing
BioComputing
Niehren, Joachim [Auteur]
BioComputing
Linking Dynamic Data [LINKS]
Versari, Cristian [Auteur]
BioComputing
Titre de la revue :
Computation
Pagination :
32
Éditeur :
MDPI
Date de publication :
2021-10-11
ISSN :
2079-3197
Mot(s)-clé(s) en anglais :
Linear equation systems
abstract interpretation
program analysis
systems biology
abstract interpretation
program analysis
systems biology
Discipline(s) HAL :
Informatique [cs]/Bio-informatique [q-bio.QM]
Résumé en anglais : [en]
We study the problem of how to compute the boolean abstraction of the solution set of a linear equation system over the positive reals. We call a linear equation system φ exact for the boolean abstraction if the abstract ...
Lire la suite >We study the problem of how to compute the boolean abstraction of the solution set of a linear equation system over the positive reals. We call a linear equation system φ exact for the boolean abstraction if the abstract interpretation of φ over the structure of booleans is equal to the boolean abstraction of the solution set of φ over the positive reals. Abstract interpretation over the booleans is thus complete for the boolean abstraction when restricted to exact linear equation systems, while it is not complete more generally. We present a new rewriting algorithm that makes 6 linear equation systems exact for the boolean abstraction while preserving the solutions over the positive reals. The rewriting algorithm is based on the elementary modes of the linear equation system. The computation of the elementary modes may require exponential time in the worst case, but is often feasible in practice with freely available tools. For exact linear equation systems we can compute the boolean abstraction by finite domain constraint programming. This yields a solution of the initial problem that is often feasible in practice. Our exact rewriting algorithm has two further applications. First, it can be used to compute the sign abstraction of linear equation systems over the reals, as needed for analysing functional programs with linear arithmetics. And second it can be applied to compute the difference abstraction of a linear equation system as used in change prediction algorithms for flux networks in systems biology.Lire moins >
Lire la suite >We study the problem of how to compute the boolean abstraction of the solution set of a linear equation system over the positive reals. We call a linear equation system φ exact for the boolean abstraction if the abstract interpretation of φ over the structure of booleans is equal to the boolean abstraction of the solution set of φ over the positive reals. Abstract interpretation over the booleans is thus complete for the boolean abstraction when restricted to exact linear equation systems, while it is not complete more generally. We present a new rewriting algorithm that makes 6 linear equation systems exact for the boolean abstraction while preserving the solutions over the positive reals. The rewriting algorithm is based on the elementary modes of the linear equation system. The computation of the elementary modes may require exponential time in the worst case, but is often feasible in practice with freely available tools. For exact linear equation systems we can compute the boolean abstraction by finite domain constraint programming. This yields a solution of the initial problem that is often feasible in practice. Our exact rewriting algorithm has two further applications. First, it can be used to compute the sign abstraction of linear equation systems over the reals, as needed for analysing functional programs with linear arithmetics. And second it can be applied to compute the difference abstraction of a linear equation system as used in change prediction algorithms for flux networks in systems biology.Lire moins >
Langue :
Anglais
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.inria.fr/hal-03384058v2/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-03384058v2/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-03384058v2/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- 2.pdf
- Accès libre
- Accéder au document