Probabilistic Model Checking for Complex Cognitive Tasks -- A case study in human-robot interaction
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.
Code (1)
Similar Papers 제목 키워드 기반
Parameterized Complexity Results for a Model of Theory of Mind Based on Dynamic Epistemic Logic
In this paper we introduce a computational-level model of theory of mind (ToM) based on dynamic epistemic logic (DEL), and we analyze its computational complexity. The model is a special case of DEL model checking. We pr…
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of…
Uncertain Process Data with Probabilistic Knowledge: Problem Characterization and Challenges
Motivated by the abundance of uncertain event data from multiple sources including physical devices and sensors, this paper presents the task of relating a stochastic process observation to a process model that can be re…
Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning
Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model checking PCTL specifications statistica…
NegationQ-Learningreinforcement-learningReinforcement Learning+1Natural Strategic Ability in Stochastic Multi-Agent Systems
Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, …