Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison
verfasst von : Pierre Roux, Pierre-Loïc Garoche
Erschienen in: FM 2014: Formal Methods
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Policy iterations have been known in static analysis since a small decade. Despite the impressive results they provide - achieving a precise fixpoint without the need of widening/narrowing mechanisms of abstract interpretation - their use is not yet widespread. Furthermore, there are basically two dual approaches: min-policies and max-policies, but they have not yet been practically compared.
Multiple issues could explain their relative low adoption in the research communities: implementation of the theory is not obvious; initialization is rarely addressed; integration with other abstraction or fixpoint engine not mentionned; etc. This paper tries to present a Policy Iteration Primer, summarizing the approaches from the practical side, focusing on their implementation and use.
We implemented both of them for a specific setting: the computation of quadratic templates, which appear useful to analyze controllers such as found in civil aircrafts or UAVs.