TITLE: Formal Methods for Partial Differential Equations
ABSTRACT: Partial differential equations (PDEs) model nearly all of the physical systems and processes of interest to scientists and engineers. The analysis of PDEs has had a tremendous impact on society by enabling our understanding of thermal, electrical, fluidic and mechanical processes. However, the study of PDEs is often approached with methods that do not allow for rigorous guarantees that a system satisfies complex design objectives. In contrast, formal methods have recently been developed to allow the formal statement of specifications, while also developing analysis techniques that can guarantee their satisfaction by design. We introduce new design methodologies that enable the systematic creation of structures whose mechanical properties, shape and functionality can be time-varying. In particular, we develop different methods for two classes of problems: (1) tunable fields, where a prescribed time evolution of the displacement field for different spatial regions of the structure is to be achieved using boundary control inputs; (2) tunable constitutive properties, where the goal is to create structures satisfying a desired stress-strain response by designing the geometry of the structure. We define appropriate spatial and temporal logics for each class of problems that allow the specification of interesting properties in a user-friendly fashion. These logics are equipped with quantitative semantics that provide a satisfaction score for the
designed structures. We use this score to formulate optimization procedures to find the best design and verify the satisfaction of the specification. Our methodologies can be applied to other processes governed by PDEs.
Calin Belta, SE/ME/CISE; Wenchao Li, SE/ECE/CISE; Harold Park, SE/ME; Ioannis Paschalidis, SE/ECE/CISE