SE PhD Prospectus Defense of Ebru Aydin Gol

Starts:
3:00 pm on Tuesday, January 22, 2013
Ends:
4:00 pm on Tuesday, January 22, 2013
Location:
110 Cummington Street, Rm 245
TITLE: FORMAL VERIFICATION AND SYNTHESIS FOR DISCRETE-TIME SYSTEMS

ABSTRACT: The proposed doctoral research aims to develop techniques to synthesize optimal control strategies for dynamical systems constrained to satisfy high-level specifications defined over predicates in their state variables. Moreover, investigation of system verification against such specifications is also aimed. The specifications are defined as linear temporal logic formulae. As opposed to “classical” control problems, in which the specifications are stability or closeness to a reference point or trajectory possibly coupled with safety, temporal logics allow for richer and more expressive specifications. Recent efforts in formal synthesis resulted in control algorithms that automatically generate such control strategies. However, the area of optimal control from temporal logic specifications is largely open.

Temporal logic specifications introduce constraints on the trajectories of the dynamical system. These constraints can be time and history dependent, and therefore, their integration in a control problem is challenging. An objective of this work is to characterize the satisfying trajectories so as to generate constraints, which can be embedded into an optimization problem. The common approach in formal synthesis is to abstract the dynamics of the system to a finite-state transition graph, and synthesize control strategies for the product of the abstraction and the specification automaton. A major contribution of this work lies in showing that a finite bisimulation quotient exists for an asymptotically stable switched linear system. Moreover, as opposed to the common approach, a language-guided procedure based on the iterative construction and refinement of an automaton that enforces satisfaction of the specification is developed. The refined automaton provides a solution to the formal synthesis problem and characterizes all satisfying system trajectories. To generate an optimal control strategy, techniques for embedding the constraints defined by such an automaton to an optimal control problem will be developed. The focus is on discrete-time linear, piece-wise affine (PWA) and switched systems. PWA and switched systems are hybrid systems with simple representation and structure, but still they are used to model a wide range of industrially relevant processes. As an application, quantitative evaluation of gene networks that are modeled as stochastic PWA systems will be studied.

COMMITTEE: Advisor: Calin Belta, SE/ME; Sean Andersson, SE/ME; David Castanon, SE/ECE; John Baillieul, SE/ME