Correct-by-Design Human-Robot Collaboration through Supervisory Control of POMDP

Human-Robot Collaboration (HRC) studies how to achieve effective collaborations between human and robots to take advantage of the flexibility from human and the autonomy from robots. Most of the existing work in HRC focused on the robot actuation design and low-level motion planning. However, many applications involving HRC, such as joint assembly manufacturing systems, need to achieve high-level tasks in a provably correct manner. In addition, many HRC applications are safety critical, such as advanced driver assistance systems and intelligent service robots. These applications motivate the requirements of HRC to have the performance guarantee to assure the task completion and safety of both human and robots.

Hence, my Ph.D. research is motivated to build a correct-by-design HRC framework that enables a performance guaranteed HRC for the safety of human and robots and the completion of high-level tasks. For such a purpose, cross-disciplinary approaches combining methods from supervisory control theory, machine learning, and computational verification are pursued. In particular, three research thrusts are structured to emphasize the requirements on uncertainties modeling, high-level task completion, and safety guarantees in HRC. To model the uncertainties from human, robots and the environment, partially observable Markov decision process (POMDP) is used as the model for HRC. With the partial observability in POMDP, the collaboration process can be described more accurately since the sensing ability of robots contains uncertainties for detections of the human behavior and the environment status. Based on the POMDP modeling, a supervisory control framework is established. With the high-level tasks described by temporal logics, an automata learning based algorithm is developed to learn a supervisor. In this process, computational verification techniques such as model checking are applied to verify the performance of the system and provide counterexamples as feedback information to improve the supervisor design. To reduce the model checking complexity, an abstraction method for POMDP is proposed to find a quotient system with a smaller size of state space. The basic idea is to iteratively refine the abstraction with counterexamples showing inconsistency between the abstract system and POMDP. Furthermore, the adaptation abilities of the supervisory control framework are discussed for POMDP modeling uncertainties and online model changing.

As the primary contribution of this dissertation, the POMDP supervisory control framework gives a high-level performance guarantee to achieve the correct-by-design HRC. A non-blocking and permissive supervisor can be automatically learned to ensure the satisfaction of high-level tasks represented by temporal logics. Beyond the theoretical work, a supervisor synthesis software is developed to combine existing formal verification packages and implement the proposed algorithms, which helps to apply the proposed POMDP supervisory control framework to different HRC applications.