SE PhD Prospectus Defense of Austin Jones

1:00 pm on Monday, May 19, 2014
3:00 pm on Monday, May 19, 2014
730 Commonwealth Avenue, Rm 301C
TITLE: Formal Methods Approaches for Estimation and Learning ABSTRACT:Formal methods are widely used in engineering to determine whether a system exhibits a certain property (verification) or to design controllers that are guaranteed to drive the system to achieve a certain property (synthesis). Most existing techniques require a large amount of accurate information about the system in order to be successful. The methods presented in this work can operate with significantly less prior information. In the domain of formal synthesis for robotics, the assumption of perfect sensing is relaxed. The resulting uncertainty is mitigated by incorporating active estimation into control policies. In contrast to model-dependent formal verification methods, the presented inference algorithms use machine learning principles to identify properties of dynamical systems from execution data alone. First, we address the problem of planning the path of a robot under temporal logic constraints (e.g. “avoid obstacles and periodically visit a recharging station”) while simultaneously minimizing the uncertainty about the state of an unknown feature of the environment (e.g. locations of fires after a natural disaster). Synthesis algorithms are presented and evaluated via simulation and experimentation. Multi-agent information gathering and persistent monitoring are considered. Second, we consider complex tasks that require gathering information about and interacting with a partially observable environment, e.g. “Maintain localization error below a certain level while also avoiding obstacles.” A new logic for these tasks is developed and the problem of synthesis is explored. Finally, we consider learning temporal logic properties of a dynamical system from a finite set of outputs. For example, given maritime surveillance data we wish to find the formula that corresponds only to those vessels that are deemed law-abiding. The inferred formulae could be used to determine automatically whether a given vessel is lawabiding or potentially law-breaking. Algorithms for performing supervised and unsupervised learning are presented. These approaches will be adapted to handle massive amounts of data. COMMITTEE: Advisor/Chair: Calin Belta, SE/ME; Mac Schwager, SE/ME; Sean Andersson, SE/ME; John Baillieul, SE/ME