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. In this dissertation new design methodologies are introduced that enable the systematic creation of structures whose mechanical properties, shape and functionality can be time-varying.

A formal methods formulation and solution to the tunable fields problem is first introduced, where a prescribed time evolution of the displacement field for different spatial regions of the structure is to be achieved using boundary control inputs. A spatial and temporal logic is defined that allows the specification of interesting properties in a user-friendly fashion and can provide a satisfaction score for the designed inputs. This score is used to formulate an optimization procedure based on Mixed Integer Programming (MIP) to find the best design.

In the second part, a sampling based assumption mining algorithm is introduced, which is the first step towards a divide and conquer strategy to solve the tunable fields problem using assume-guarantee contracts. The algorithm produces a temporal logic formula that represents initial conditions and external inputs of a system that satisfy a goal given as a temporal logic formula over its state. An online supervised learning algorithm is presented, based on decision tree learning, that is used to produce a temporal logic formula from assumption samples.

The third part focuses on the tunable constitutive properties problem, where the goal is to create structures satisfying a stress-strain response by designing their geometry. The goal is represented as a logic formula that captures the allowed deviation from a reference and provides a satisfaction score. An optimization procedure is used to obtain the best geometric design.