Assume-guarantee reasoning framework for MDP-POMDP

Abstract

We propose an assume-guarantee reasoning (AGR) framework for verification problem of a system with two components modeled by Markov Decision Process (MDP) and Partially Observable MDP (POMDP), respectively. MDP-POMDP model describes system's sensing, actuation and environment uncertainties, which can be used in the modeling of systems containing different subsystems, e.g., human-robot collaboration process. While the verification problem of MDP-POMDP asks whether or not a specification can be satisfied by the regulated behavior under certain control policies, our main contribution in this paper is to present and prove a sound and complete AGR rule based on POMDP strong simulation relation to reduce the verification complexity.