Sparsity in the coefficients of a semidefinite program has important implications for the structure (sparsity and rank) of the solutions of the problem. The talk will focus on applications of classical results in sparse matrix theory, and, in particular, the fact that, for chordal sparsity patterns, zero-fill Cholesky factorizations, maximum-determinant and minimum-rank positive semidefinite completions, and minimum-dimension Euclidean distance matrix completions are simple to characterize and easy to compute. These properties are very useful in theoretical analysis and algorithm development for semidefinite optimization. Data structures and techniques familiar from the sparse matrix literature, such as elimination trees, supernodal elimination trees, and multifrontal algorithms, will play a central role in the derivation of the key results and algorithms.
Semidefinite programming (SDP) solvers are increasingly used as primitives in many program verification tasks to synthesize and verify polynomial invariants for a variety of systems including programs, hybrid systems and stochastic models. On one hand, they provide a tractable alternative to reasoning about semi-algebraic constraints. However, the results are often unreliable due to ``numerical issues'' that include a large number of reasons such as floating-point errors, ill-conditioned problems, failure of strict feasibility, and more generally, the specifics of the algorithms used to solve SDPs. These issues influence whether the final numerical results are trustworthy or not. In this paper, we briefly survey the emerging use of SDP solvers in the static analysis community. We report on the perils of using SDP solvers for common invariant synthesis tasks, characterizing the common failures that can lead to unreliable answers. Next, we demonstrate existing tools for guaranteed semidefinite programming that often prove inadequate to our needs. Finally, we present a solution for verified semidefinite programming that can be used to check the reliability of the solution output by the solver and a padding procedure that can check the presence of a feasible nearby solution to the one output by the solver. We report on some successful preliminary experiments involving our padding procedure.
The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical proofs on on-line optimization programs which can be leveraged to assist in the development and verification of their implementation. To demonstrate this we wrote a C implementation of a primal algorithm solving a small linear problem. We annotated this small example with proof elements in a specific language call ACSL. Using this language enable a software call Frama-C to guarantee that the C code is satisfying all the property stated as annotation such as termination or correctness.
Wednesday, September 21, 2016
This talk will focus on using theory of controlled Markov chains to synthesize higher-level control laws for autonomous systems, particularly multi-agent autonomous systems, e.g., swarms. The proposed approach specifies the time evolution of the probability density distribution of the vehicles by using a Markov chain, which guides the vehicles to a desired steady-state distribution, while satisfying the prescribed ergodicity, motion, and safety constraints. We present convex optimization methods for both offline and online Markov chain synthesis. We extend these results to Markov Decision Processes (MDPs), and present results on safety constrained MDP policy synthesis. We also incorporate additional observations for instantaneous transitions in MDPs, to extend the convex MDP synthesis results to vehicles with ON/OFF observation modes.
We consider the problem of a maneuvering vehicle performing a rejoin to close formation with another maneuvering vehicle. The dynamics of relative position and velocity is shown to be governed by a linear time varying dynamics. Using rotationally invariant potential functions to exploit the symmetry present in the dynamics, we are able to construct Lyapunov functions that, along with their time derivative, are independent of time allowing us to conclude, in the case of linear feedback, exponential stability of the time varying closed loop system. The situation with nonlinear feedback is somewhat more delicate, requiring the use of Matrosov's theorem to prove uniform global asymptotic stability. Performance of the approach is illustrated by rejoining to an aggressively maneuvering flight leader using a saturating control law.
I will review some known positivity certificates for real polynomials or more general function algebras. Then I will discuss some challenging questions involving positive polynomials: The BMV conjecture and its recent solution by Stahl, Crouzeix bound for the numerical range of functions of matrices and some geometrical aspects of Cauchy-Riemann manifolds.
In this talk we present an overview of several symbolic-numeric algorithms and software tools developed for applications in optimal control and robust space mission design. We aim at providing computer-aided proofs of numerical values, with validated and reasonably tight error bounds, without sacrificing efficiency. We focus on two applications. Firstly, due to the large amount of debris, we consider the computation of collision probabilities between space objects in low Earth orbits. Secondly, we consider the spacecraft rendezvous problem: under certain assumptions, we are interested in designing a fuel-optimal maneuvers plan, which takes one active spacecraft, originally moving on an initial orbit, to the final reference orbit of a passive target spacecraft e.g., International Space Station. In these applications, we particularly make use of properties of D-finite functions (solutions of linear differential equations with polynomial coefficients) and analytic or validated bounds on truncation errors for power or Chebyshev series. This talk is based on joint works with D. Arzelier, F. Bréhard, N. Brisebarre, J.-B. Lasserre, C. Louembet, A. Rondepierre, B. Salvy, R. Serra.
Thursday, September 22, 2016
From 1930 to 1960, command and control systems were implemented electro-mechanically and evidence of proper behavior were written by hand.
From 1960 to 2000, command and control systems were implemented on a computer and evidence of proper behavior, though sometimes computed with the help of a computer, were still written by hand.
From 2000 onwards, command and control systems are still implemented on a computer. This talk argues that evidence of proper behavior is necessary and should now be written by a computer. To support this view, the case of classical control systems will be considered first, followed by convex optimization algorithms that can be used for advanced vehicle guidance. The development of a dedicated and formal, computer-ready meta-language supporting the expression of proofs of proper behavior of these systems will be discussed in conjunction with existing general mathematical reasoning languages. Practical examples will be discussed to root this research topic into real-life systems and concerns.
A combination of a policy iterations algorithm and quadratic templates was proposed in 2010 to represent reachable values set of linear systems as an intersection of ellipsoids. However, this combination suffered from the fact that the quadratic templates had to be provided by the user. Then in 2014, an automatic generation of quadratic templates from quadratic Lyapunov functions was proposed. In this talk, we present a new automatic construction of quadratic templates. Each template is associated to a coordinate of the state-variable and minimizes a quadratic optimization problem. This new construction coupled with the policy iterations algorithm leads to a tighter representation of the reachable values set.