2016/10/28 by Sebastian Junges, Nils Jansen, Junges, Sebastian +5
Computer Science · #AI-based Problem Solving and Planning #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Methods in Verification #Reinforcement Learning in Robotics #Robotics (cs.RO)
paper · pdf · doi:10.48550/arxiv.1610.09409
openalex publication_date 2016/10/28 · openalex created_date 2016/11/11 · openalex updated_date 2026/07/28
This paper proposes to use probabilistic model checking to synthesize optimal robot policies in multi-tasking autonomous systems that are subject to human-robot interaction. Given the convincing empirical evidence that human behavior can be related to reinforcement models, we take as input a well-studied Q-table model of the human behavior for flexible scenarios. We first describe an automated procedure to distill a Markov decision process (MDP) for the human in an arbitrary but fixed scenario. The distinctive issue is that -- in contrast to existing models -- under-specification of the human behavior is included. Probabilistic model checking is used to predict the human's behavior. Finally, the MDP model is extended with a robot model. Optimal robot policies are synthesized by analyzing the resulting two-player stochastic game. Experimental results with a prototypical implementation using PRISM show promising results.