Yushan Chen, 23 January 2013

Yushan Chen, a PhD candidate in Hybrid and Networked Systems at Boston University, will be visiting campus the 23rd of January (Wed). Please sign up for a time to meet with her, including a location.

Wednesday, January 23rd

• 9:30 am: Richard
• 10 am: Eric Wolff (Steele 110)
• 10:45 am: Open
• 11:30 am - grab lunch
• 12-2: NCS group meeting
• 2-3: seminar to NCS group
• 3-4: CDS tea
• 4:00 pm: Scott Livingston (meeting at a whiteboard in Annenberg or Steele)
• 4:45: Necmiye (130 Steele)
• 5:30 pm: meeting with Richard
• 6:00 pm: done

Abstract:

In formal verification, simple models of software programs and digital circuits are checked against temporal logic properties such as safety (ie., something bad never happens) and liveness (ie., something good eventually happens). While formal verification received a lot of attention, the problem of formal synthesis, where the focus is to construct a provably-correct system (eg., safe by design) is still in its infancy. We propose theoretical frameworks and computational tools for automatic synthesis of robot controllers that are correct-by-construction from specifications given in rich, human-like languages. We consider deterministic, probabilistic, and partially unknown scenarios, in which the dynamics of each robot is modeled as a finite transition system, Markov decision process, and game transition system, respectively. These models allow for the use of (adapted) formal languages as specification languages, tools from formal verification resembling model checking, and different techniques inspired from results in concurrency theory, approximate DP, automata-learning for synthesis of provably-correct control and communication strategies. We apply the developed algorithms and frameworks to deploy robots in Khepera-based testbeds (i.e., robotic urban-like and indoor-like environments).