More Like this

1. Pegasus: A framework for sound continuous invariant generation.

   https://doi.org/10.1007/978-3-030-30942-8_10  

   Sogokon, Andrew; Mitsch, Stefan; Tan, Yong Kiam; Cordwell, Katherine; Platzer, André (September 2019, FM Symposium on Formal Methods)

   Continuous invariants are an important ingredient for deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges for automating formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks. 

   more » « less
2. Machine-assisted discovery of integrable symplectic mappings

   https://doi.org/10.1103/PhysRevResearch.5.043241  

   Zolkin, T.; Kharkov, Y.; Nagaitsev, S. (December 2023, Physical Review Research)

   We present a new automated method for finding integrable symplectic maps of the plane. These dynamical systems possess a hidden symmetry associated with an existence of conserved quantities, i.e., integrals of motion. The core idea of the algorithm is based on the knowledge that the evolution of an integrable system in the phase space is restricted to a lower-dimensional submanifold. Limiting ourselves to polygon invariants of motion, we analyze the shape of individual trajectories thus successfully distinguishing integrable motion from chaotic cases. For example, our method rediscovers some of the famous McMillan-Suris integrable mappings and ultradiscrete Painlevé equations. In total, over 100 new integrable families are presented and analyzed; some of them are isolated in the space of parameters, and some of them are families with one parameter (or the ratio of parameters) being continuous or discrete. At the end of the paper, we suggest how newly discovered maps are related to a general 2D symplectic map via an introduction of discrete perturbation theory and propose a method on how to construct smooth near-integrable dynamical systems based on mappings with polygon invariants. 

   more » « less
3. Design of smooth hybrid controllers for a class of non‐linear systems

   https://doi.org/10.1049/iet-cta.2019.1112  

   Shamgah, Laya; Getahun_Tadewos, Tadewos; Karimoddini, Ali (February 2021, IET Control Theory & Applications)

   Symbolic planning techniques rely on abstract information about a continuous system to design a discrete planner to satisfy desired high‐level objectives. However, applying the generated discrete commands of the discrete planner to the original system may face several challenges, including real‐time implementation, preserving the properties of high‐level objectives in the continuous domain, and issues such as discontinuity in control signals that may physically harm the system. To address these issues and challenges, the authors proposed a novel hybrid control structure for systems with non‐linear multi‐affine dynamics over rectangular partitions. In the proposed framework, a discrete planner can be separately designed to achieve high‐level specifications. Then, the proposed hybrid controller generates jumpless continuous control signals to drive the system over the partitioned space executing the discrete commands of the planner. The hybrid controller generates continuous signals in real‐time while respecting the dynamics of the system and preserving the desired objectives of the high‐level plan. The design process is described in detail and the existence and uniqueness of the proposed solution are investigated. Finally, several case studies are provided to verify the effectiveness of the developed technique. 

   more » « less
4. Hybrid Event Shaping to Stabilize Periodic Hybrid Orbits

   Zhu, James; Kong, Nathan J.; Council, George; Johnson, Aaron M. (May 2022, IEEE International Conference on Robotics and Automation)

   Many controllers for legged robotic systems leverage open- or closed-loop control at discrete hybrid events to enhance stability. These controllers appear in several well studied phenomena such as the Raibert stepping controller, paddle juggling, and swing leg retraction. This work introduces hybrid event shaping (HES): a generalized method for analyzing and designing stable hybrid event controllers. HES utilizes the saltation matrix, which gives a closed-form equation for the effect that hybrid events have on stability. We also introduce shape parameters, which are higher order terms that can be tuned completely independently of the system dynamics to promote stability. Optimization methods are used to produce values of these parameters that optimize a stability measure. Hybrid event shaping captures previously developed control methods while also producing new optimally stable trajectories without the need for continuous-domain feedback. 

   more » « less
5. Making thermodynamic models of mixtures predictive by machine learning: matrix completion of pair interactions

   https://doi.org/10.1039/D1SC07210B  

   Jirasek, Fabian; Bamler, Robert; Fellenz, Sophie; Bortz, Michael; Kloft, Marius; Mandt, Stephan; Hasse, Hans (May 2022, Chemical Science)

   Predictive models of thermodynamic properties of mixtures are paramount in chemical engineering and chemistry. Classical thermodynamic models are successful in generalizing over (continuous) conditions like temperature and concentration. On the other hand, matrix completion methods (MCMs) from machine learning successfully generalize over (discrete) binary systems; these MCMs can make predictions without any data for a given binary system by implicitly learning commonalities across systems. In the present work, we combine the strengths from both worlds in a hybrid approach. The underlying idea is to predict the pair-interaction energies , as they are used in basically all physical models of liquid mixtures, by an MCM. As an example, we embed an MCM into UNIQUAC, a widely-used physical model for the Gibbs excess energy. We train the resulting hybrid model in a Bayesian machine-learning framework on experimental data for activity coefficients in binary systems of 1146 components from the Dortmund Data Bank. We thereby obtain, for the first time, a complete set of UNIQUAC parameters for all binary systems of these components, which allows us to predict, in principle, activity coefficients at arbitrary temperature and composition for any combination of these components, not only for binary but also for multicomponent systems. The hybrid model even outperforms the best available physical model for predicting activity coefficients, the modified UNIFAC (Dortmund) model. 

   more » « less