Abstract
With the increasing role of human-in-the-loop (HITL) based autonomous systems, researchers have made several attempts to understand how an operator's performance is affected by various parameters. In such systems, the performance of the operator directly influences the overall system performance. Although operator performance has been extensively studied at various psychological, behavioral, and physical levels, to the best of our knowledge there is a lack of literature addressing how a variety of operator's internal characteristics and external environmental factors affect the performance of the system for various mission objectives. This paper addresses this issue and proposes a probabilistic model checking based approach to assess the performance of an HITL-based autonomous system. We model the system as a Markov decision process and use probabilistic model checking to assess the impact of various operator and environment parameters on application-specific mission objectives. In addition to considering key operator characteristics in the fatigue model, the proposed method captures dynamic workload, task type, and the impact of various break policies on overall mission objectives. The model can be adapted to carry out system analysis at a higher level of abstraction for a variety of applications. The proposed method is applied to assess various scenarios in a case study from the literature. The results obtained using the proposed method can help a system designer evaluate the impact of various operator and environment characteristics to improve application-specific mission objectives.