Probabilistic Model Checking for Complex Cognitive Tasks -- A case study in human-robot interaction
This work addresses the challenge of under-specified human behavior in human-robot interaction for autonomous systems, representing an incremental advancement by applying existing probabilistic model checking methods to a new domain.
The paper tackles the problem of synthesizing optimal robot policies in multi-tasking autonomous systems with human-robot interaction by using probabilistic model checking to model human behavior as a Markov decision process and extending it to a two-player stochastic game. Experimental results with a PRISM implementation show promising outcomes, though no concrete numbers are provided.
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.