[FWHT15] Lu Feng, Clemens Wiltsche, Laura Humphrey and Ufuk Topcu. Controller Synthesis for Autonomous Systems Interacting with Human Operators. In Proc. International Conference on Cyber-Physical Systems (ICCPS'15), ACM. 2015. [pdf] [Uses PRISM and PRISM-games to synthesize control protocols for autonomous systems interacting with human operators.]
Downloads:  pdf pdf (744 KB)
Abstract. We propose an approach to synthesize control protocols for autonomous systems that account for uncertainties and imperfections in interactions with human operators. As an illustrative example, we consider a scenario involving road network surveillance by an unmanned aerial vehicle (UAV) that is controlled remotely by a human operator but also has a certain degree of autonomy. Depending on the type (i.e., probabilistic and/or nondeterministic) of knowledge about the uncertainties and imperfections in the operator-autonomy interactions, we use abstractions based on Markov decision processes and augment these models to stochastic two-player games. Our approach enables the synthesis of operator-dependent optimal mission plans for the UAV, highlighting the effects of operator characteristics (e.g., work- load, proficiency, and fatigue) on UAV mission performance; it can also provide informative feedback (e.g., Pareto curves showing the trade-offs between multiple mission objectives), potentially assisting the operator in decision-making.