• TITLE: Complexity in Automation of SOS Proofs: An Illustrative Example
• AUTHORS: Dennice Gayme, Maryam Fazel, John Doyle, .
• ABSTRACT: We present a case study in proving invariance for a chaotic dynamical system, the logistic map, based on Positivstellensatz refutations, with the aim of studying the problems associated with developing a completely automated proof system. We derive the refutation using two different forms of the Positivstellensatz and compare the results to illustrate the challenges in defining and classifying the `complexity' of such a proof. The results show the flexibility of the SOS framework in converting a dynamics problem into a semialgebraic one as well as in choosing the form of the proof. Yet it is this very flexibility that complicates the process of automating the proof system and classifying proof `complexity.'
• STATUS: Proc. of Conference on Decision and Control, Dec 2006.
• paper: pdf file