An Approach to Modeling Cybersickness and Task Performance in Augmented Reality Using Discrete-Time Markov Chains

Cybersickness is a major challenge to the reliable use of augmented reality (AR) systems, as it can impair operators’ cognition and task performance. However, existing cybersickness models primarily rely on predictive approaches and lack formally verifiable methods to assess cybersickness and its impact on task performance. This paper introduces a formal modeling approach using Discrete-Time Markov Chains (DTMC) to represent the temporal progression of cybersickness and its impact on task performance in a checkpoint surveillance scenario. The model incorporates exposure duration as a key cybersickness-inducing factor and uses preliminary experimental data to generate mock datasets for model construction and verification. The model enables probabilistic verification of properties, such as bounds on the onset of cybersickness and task performance. This approach demonstrates the feasibility of applying formal methods to model human interaction with AR systems and to generate probabilistic guarantees on operators’ cybersickness and task performance.