Accelerated fixpoint iteration by means of widening and narrowing is the method of choice for solving systems of equations over domains with infinite ascending chains. The strict separation into an ascending widening and a descending narrowing phase, however, may unnecessarily give up precision that cannot be recovered later. It is also unsuitable for equation systems with infinitely many unknowns — where local solving must be used. As a remedy, we present a novel operator ⍁ that combines a given widening operator ∇ with a given narrowing operator Δ. We present adapted versions of round-robin and worklist iteration as well as local and side-effecting solving algorithms for the combined operator ⍁. We prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns are encountered.

Efficiently intertwining widening and narrowing

AMATO, Gianluca;SCOZZARI, Francesca;
2016

Abstract

Accelerated fixpoint iteration by means of widening and narrowing is the method of choice for solving systems of equations over domains with infinite ascending chains. The strict separation into an ascending widening and a descending narrowing phase, however, may unnecessarily give up precision that cannot be recovered later. It is also unsuitable for equation systems with infinitely many unknowns — where local solving must be used. As a remedy, we present a novel operator ⍁ that combines a given widening operator ∇ with a given narrowing operator Δ. We present adapted versions of round-robin and worklist iteration as well as local and side-effecting solving algorithms for the combined operator ⍁. We prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns are encountered.
File in questo prodotto:
File Dimensione Formato  
preprint.pdf

accesso aperto

Tipologia: Documento in Pre-print
Dimensione 502.53 kB
Formato Adobe PDF
502.53 kB Adobe PDF Visualizza/Apri
scp16.pdf

Solo gestori archivio

Descrizione: Article
Tipologia: PDF editoriale
Dimensione 760.07 kB
Formato Adobe PDF
760.07 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11564/662756
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 15
social impact