Difference between revisions of "Yushan Chen, 23 January 2013"

From MurrayWiki
Jump to: navigation, search
(Created page with "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 h...")
 
(Wednesday, January 23rd)
 
(8 intermediate revisions by 5 users not shown)
Line 3: Line 3:
 
=== Wednesday, January 23rd ===
 
=== Wednesday, January 23rd ===
  
* 9:30 am: Richard
+
* 9:20 am: Richard, 109 Steele Lab
* 10 am: Open
+
* 9:50 am: Anissa (travel reimbursements), 107 Steele Lab
* 10:30 am: Open
+
* 10 am: Eric Wolff (Steele 110)
* 11:00 am: Open
+
* 10:45 am: Open
 
* 11:30 am - grab lunch
 
* 11:30 am - grab lunch
 
* 12-2: NCS group meeting
 
* 12-2: NCS group meeting
 
* 2-3: seminar to NCS group
 
* 2-3: seminar to NCS group
 
* 3-4: CDS tea
 
* 3-4: CDS tea
* 4:00 pm: Open
+
* 4:00 pm: Scott Livingston (meeting at a whiteboard in Annenberg or Steele)
* 4:30: Open
+
* 4:45: Necmiye (130 Steele Lab)
* 5:00 pm: Open
+
* 5:30 pm: wrapup meeting with Richard (109 Steele)
* 5:30 pm: meeting with Richard
+
* 6:00 pm: done (might be 6:30 pm if Richard is running late)
* 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).

Latest revision as of 04:50, 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:20 am: Richard, 109 Steele Lab
  • 9:50 am: Anissa (travel reimbursements), 107 Steele Lab
  • 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 Lab)
  • 5:30 pm: wrapup meeting with Richard (109 Steele)
  • 6:00 pm: done (might be 6:30 pm if Richard is running late)

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).