A linguistic method for robot verification programming and control
Dantam, Neil Thomas
MetadataShow full item record
There are many competing techniques for specifying robot policies, each having advantages in different circumstances. To unify these techniques in a single framework, we use formal language as an intermediate representation for robot behavior. This links previously disparate techniques such as temporal logics and learning from demonstration, and it links data driven approaches such as semantic mapping with formal discrete event and hybrid systems models. These formal models enable system verification -- a crucial point for physical robots. We introduce a set of rewrite rules for hybrid systems and apply it automatically build a hybrid model for mobile manipulation from a semantic map. In the manipulation domain, we develop a new workspace interpolation methods which provides direct, non-stop motion through multiple waypoints, and we introduce a filtering technique for online camera registration to avoid static calibration and handle changing camera positions. To handle concurrent communication with embedded robot hardware, we develop a new real-time interprocess communication system which offers lower latency than Linux sockets. Finally, we consider how time constraints affect the execution of systems modeled hierarchically using context-free grammars. Based on these constraints, we modify the LL(1) parser generation algorithm to operate in real-time with bounded memory use.