More Like this

1. Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates

   https://doi.org/https://doi.org/10.1007/978-3-030-32430-8_23  

   Ramasubramanian, B; Niu, L.; Clark, A; Bushnell, L; Poovendran, R (January 2019, IEEE Conference on Decision and Game Theory for Security)

   This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discretetime dynamics. The temporal logic specification is given in safe−LTLF , a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zerosum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximizes the probability of satisfaction of a safe − LTLF formula over a finite time-horizon under any stationary adversary policy. We introduce secure control barrier certificates (S-CBCs), a generalization of barrier certificates and control barrier certificates that accounts for the presence of an adversary, and use S-CBCs to provide a lower bound on the above satisfaction probability. When the dynamics of the evolution of the system state has a specific underlying structure, we present a way to determine an S-CBC as a polynomial in the state variables using sum-of-squares optimization. An illustrative example demonstrates our approach. 

   more » « less
2. An Exponentially Convergent Primal-Dual Algorithm for Nonsmooth Composite Minimization

   https://doi.org/10.1109/CDC.2018.8619760  

   Ding, Dongsheng; Hu, Bin; Dhingra, Neil K.; Jovanovic, Mihailo R. (December 2018, 2018 IEEE Conference on Decision and Control (CDC))

   We consider a class of nonsmooth convex composite optimization problems, where the objective function is given by the sum of a continuously differentiable convex term and a potentially non-differentiable convex regularizer. In [1], the authors introduced the proximal augmented Lagrangian method and derived the resulting continuous-time primal-dual dynamics that converge to the optimal solution. In this paper, we extend these dynamics from continuous to discrete time via the forward Euler discretization. We prove explicit bounds on the exponential convergence rates of our proposed algorithm with a sufficiently small step size. Since a larger step size can improve the convergence speed, we further develop a linear matrix inequality (LMI) condition which can be numerically solved to provide rate certificates with general step size choices. In addition, we prove that a large range of step size values can guarantee exponential convergence. We close the paper by demonstrating the performance of the proposed algorithm via computational experiments. 

   more » « less
3. Sparse identification of nonlocal interaction kernels in nonlinear gradient flow equations via partial inversion

   https://doi.org/10.1142/S0218202525500137  

   Carrillo, José A; Estrada-Rodriguez, Gissell; Mikolás, László; Tang, Sui (May 2025, Mathematical Models and Methods in Applied Sciences)

   We address the inverse problem of identifying nonlocal interaction potentials in nonlinear aggregation–diffusion equations from noisy discrete trajectory data. Our approach involves formulating and solving a regularized variational problem, which requires minimizing a quadratic error functional across a set of hypothesis functions, further augmented by a sparsity-enhancing regularizer. We employ a partial inversion algorithm, akin to the CoSaMP and subspace pursuit algorithms, to solve the basis pursuit problem. A key theoretical contribution is our novel stability estimate for the PDEs, validating the error functional ability in controlling the 2-Wasserstein distance between solutions generated using the true and estimated interaction potentials. Our work also includes an error analysis of estimators caused by discretization and observational errors in practical implementations. We demonstrate the effectiveness of the methods through various 1D and 2D examples showcasing collective behaviors. 

   more » « less
4. DECOUPLED, LINEAR, AND ENERGY STABLE FINITE ELEMENT METHOD FOR THE CAHN–HILLIARD–NAVIER–STOKES–DARCY PHASE FIELD MODEL

   Gao, Y; He, X; Mei, L; Yang, X. (January 2018, SIAM journal on scientific computing)

   In this paper, we consider the numerical approximation for a phase field model of the coupled two-phase free flow and two-phase porous media flow. This model consists of Cahn– Hilliard–Navier–Stokes equations in the free flow region and Cahn–Hilliard–Darcy equations in the porous media region that are coupled by seven interface conditions. The coupled system is decoupled based on the interface conditions and the solution values on the interface from the previous time step. A fully discretized scheme with finite elements for the spatial discretization is developed to solve the decoupled system. In order to deal with the difficulties arising from the interface conditions, the decoupled scheme needs to be constructed appropriately for the interface terms, and a modified discrete energy is introduced with an interface component. Furthermore, the scheme is linearized and energy stable. Hence, at each time step one need only solve a linear elliptic system for each of the two decoupled equations. Stability of the model and the proposed method is rigorously proved. Numerical experiments are presented to illustrate the features of the proposed numerical method and verify the theoretical conclusions. 

   more » « less
5. 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