Yushan Chen, 23 January 2013: Difference between revisions
No edit summary |
|||
| Line 14: | Line 14: | ||
* 4:45: Necmiye (130 Steele Lab) | * 4:45: Necmiye (130 Steele Lab) | ||
* 5:30 pm: wrapup meeting with Richard (109 Steele) | * 5:30 pm: wrapup meeting with Richard (109 Steele) | ||
* 6:00 pm: done | * 6:00 pm: done (might be 6:30 pm if Richard is running late) | ||
Abstract | 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). | 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). | ||
Revision as of 20:21, 20 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:15 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).
