EmoSTL: Formal Spatial-Temporal Verification of Emotion Specifications in Computer Games

As the game industry continues to evolve in pop-ularity, testing the experience of players becomes crucial for attracting and retaining players in the highly competitive market. However, the absence of automated methods for articulating and verifying player experience (PX) specifications led us to introduce EmoSTL, a specialized language that extends Linear Temporal Logic with spatial and time-interval expressions, enabling the capture of complex temporal and spatial aspects of players' emotions and their experiences within games. We conducted a user study to collect suggestive PX requirements for a game under test to assess the capabilities of EmoSTL. Findings reveal that the language formalizes 92 percent of the set PX requirements, and with runtime verification, several PX design issues are iden-tified in the game. Moreoever, EmoSTL performance evaluation demonstrates its linear execution time, showcasing the language potential usage in automated PX testing of games.