Exact Boolean Abstraction of Linear Equation Systems
Résumé
We study the problem of how to compute the boolean abstraction of the solution set of 1 a linear equation system over the positive reals. We call a linear equation system φ exact for the 2 boolean abstraction if the abstract interpretation of φ over the structure of booleans is equal to the 3 boolean abstraction of the solution set of φ over the positive reals. Abstract interpretation over 4 the booleans is thus complete for the boolean abstraction when restricted to exact linear equation 5 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 7 positive reals. The rewriting algorithm is based on the elementary modes of the linear equation 8 system. The computation of the elementary modes may require exponential time in the worst 9 case, but is often feasible in practice with freely available tools. For exact linear equation systems 10 we can compute the boolean abstraction by finite domain constraint programming. This yields a 11 solution of the initial problem that is often feasible in practice. Our exact rewriting algorithm has 12 two further applications. First, it can be used to compute the sign abstraction of linear equation 13 systems over the reals, as needed for analysing function programs with linear arithmetics. And 14 second it can be applied to compute the difference abstraction of a linear equation system as used 15 in change prediction algorithms for flux networks in systems biology.
Origine : Fichiers produits par l'(les) auteur(s)