More Like this

1. Vector barrier certificates and comparison systems

   https://doi.org/10.1007/978-3-319-95582-7_25  

   Sogokon, Andrew; Ghorbal, Khalil; Tan, Yong Kiam; Platzer, Andre (July 2018, FM 2018: Formal Methods - 22nd International Symposium, Oxford, UK, July 15-17, 2018, Proceedings)

   Vector Lyapunov functions are a multi-dimensional extension of the more familiar (scalar) Lyapunov functions, commonly used to prove stability properties in systems described by non-linear ordinary differential equations (ODEs). This paper explores an analogous vector extension for so-called barrier certificates used in safety verification. As with vector Lyapunov functions, the approach hinges on constructing appropriate comparison systems, i.e., related differential equation systems from which properties of the original system may be inferred. The paper presents an accessible development of the approach, demonstrates that most previous notions of barrier certificate are special cases of comparison systems, and discusses the potential applications of vector barrier certificates in safety verification and invariant synthesis. 

   more » « less
2. Algorithmic Thresholds for Refuting Random Polynomial Systems

   https://doi.org/10.1137/1.9781611977073.49  

   Hsieh, Tim; Kothari, Pravesh K. (January 2022, Proceedings of the annual ACMSIAM symposium on discrete algorithms)

   Consider a system of m polynomial equations {pi(x)=bi}i≤m of degree D≥2 in n-dimensional variable x∈ℝn such that each coefficient of every pi and bis are chosen at random and independently from some continuous distribution. We study the basic question of determining the smallest m -- the algorithmic threshold -- for which efficient algorithms can find refutations (i.e. certificates of unsatisfiability) for such systems. This setting generalizes problems such as refuting random SAT instances, low-rank matrix sensing and certifying pseudo-randomness of Goldreich's candidate generators and generalizations. We show that for every d∈ℕ, the (n+m)O(d)-time canonical sum-of-squares (SoS) relaxation refutes such a system with high probability whenever m≥O(n)⋅(nd)D−1. We prove a lower bound in the restricted low-degree polynomial model of computation which suggests that this trade-off between SoS degree and the number of equations is nearly tight for all d. We also confirm the predictions of this lower bound in a limited setting by showing a lower bound on the canonical degree-4 sum-of-squares relaxation for refuting random quadratic polynomials. Together, our results provide evidence for an algorithmic threshold for the problem at m≳O˜(n)⋅n(1−δ)(D−1) for 2nδ-time algorithms for all δ. 

   more » « less
3. Asymptotically Kasner-like singularities

   https://doi.org/10.1353/ajm.2023.a902957  

   Fournodavlos, Grigorios; Luk, Jonathan (August 2023, American Journal of Mathematics)

   abstract: We prove existence, uniqueness and regularity of solutions to the Einstein vacuum equations taking the form $$ {}^{(4)}g = -dt^2 + \sum_{i,j=1}^3 a_{ij}t^{2 p_{\max\{i,j\}}}\,{\rm d} x^i\,{\rm d} x^j $$ on $$(0,T]_t\times\Bbb{T}^3_x$$, where $$a_{ij}(t,x)$$ and $$p_i(x)$$ are regular functions without symmetry or analyticity assumptions. These metrics are singular and asymptotically Kasner-like as $$t\to 0^+$$. These solutions are expected to be highly non-generic, and our construction can be viewed as solving a singular initial value problem with Fuchsian-type analysis where the data are posed on the ``singular hypersurface'' $$\{t=0\}$$. This is the first such result without imposing symmetry or analyticity. To carry out the analysis, we study the problem in a synchronized coordinate system. In particular, we introduce a novel way to perform (weighted) energy estimates in such a coordinate system based on estimating the second fundamental forms of the constant-$$t$$ hypersurfaces. 

   more » « less
4. Closure Certificates

   Murali, V; Trivedi, A; Zamani, M (May 2024, In 27th ACM International Conference on Hybrid Systems: Computation and Control (HSCC ’24),)

   A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an in- ductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures— such as sum-of-squares programming (SOS) or satisfiability-modulo- theory solvers (SMT)—barrier certificates enable an automated de- ductive verification approach to safety. The barrier certificate ap- proach has been extended to refute LTL and l -regular specifications by separating consecutive transitions of corresponding l -automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We aug- ment these definitions with SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness over some case studies. 

   more » « less
5. Tensor Completion with Nearly Linear Samples Given Weak Side Information

   https://doi.org/10.1145/3530905  

   Yu, Christina Lee; Xi, Xumei (May 2022, Proceedings of the ACM on Measurement and Analysis of Computing Systems)

   Tensor completion exhibits an interesting computational-statistical gap in terms of the number of samples needed to perform tensor estimation. While there are only Θ(tn) degrees of freedom in a t-order tensor with n^t entries, the best known polynomial time algorithm requires O(n^t/2 ) samples in order to guarantee consistent estimation. In this paper, we show that weak side information is sufficient to reduce the sample complexity to O(n). The side information consists of a weight vector for each of the modes which is not orthogonal to any of the latent factors along that mode; this is significantly weaker than assuming noisy knowledge of the subspaces. We provide an algorithm that utilizes this side information to produce a consistent estimator with O(n^1+κ ) samples for any small constant κ > 0. We also provide experiments on both synthetic and real-world datasets that validate our theoretical insights. 

   more » « less