TY - JOUR
T1 - Solving systems of rational equations through strategy iteration
AU - Gawlitza, Thomas Martin
AU - Seidl, Helmut
PY - 2011/4
Y1 - 2011/4
N2 - We present practical algorithms for computing exact least solutions of equation systems over the reals with addition, multiplication by positive constants, minimum and maximum. The algorithms are based on strategy iteration. Our algorithms can, for instance, be used for the analysis of recursive stochastic games. In the present article we apply our techniques for computing abstract least fixpoint semantics of affine programs over the relational template polyhedra domain. In particular, we thus obtain practical algorithms for computing abstract least fixpoint semantics over the abstract domains of intervals, zones, and octagons.
AB - We present practical algorithms for computing exact least solutions of equation systems over the reals with addition, multiplication by positive constants, minimum and maximum. The algorithms are based on strategy iteration. Our algorithms can, for instance, be used for the analysis of recursive stochastic games. In the present article we apply our techniques for computing abstract least fixpoint semantics of affine programs over the relational template polyhedra domain. In particular, we thus obtain practical algorithms for computing abstract least fixpoint semantics over the abstract domains of intervals, zones, and octagons.
KW - Abstract interpretation
KW - Fixpoint equation systems
KW - Recursive stochastic games
KW - Static program analysis
KW - Strategy improvement algorithms
UR - http://www.scopus.com/inward/record.url?scp=79955676587&partnerID=8YFLogxK
U2 - 10.1145/1961204.1961207
DO - 10.1145/1961204.1961207
M3 - Article
AN - SCOPUS:79955676587
SN - 0164-0925
VL - 33
JO - ACM Transactions on Programming Languages and Systems (TOPLAS)
JF - ACM Transactions on Programming Languages and Systems (TOPLAS)
IS - 3
M1 - 11
ER -