FindMe: A Prototype Videogame AI based on CTL with an Optimized Synthesis Algorithm

Marco Aruta (University of Naples Federico II), Vadim Malvone (Télécom Paris), Aniello Murano (University of Naples Federico II), Vincenzo Pio Palma (University of Naples Federico II), Salvatore Romano (University of Naples Federico II)

Abstract

We present FindMe, a prototype tool that enhances AI-driven decisionmaking in Non-Player Characters (NPCs) within Unreal Engine 5.4. Our approach utilizes formal verification techniques, specifically Computation Tree Logic (CTL), to enable real-time adaptive behavior in NPCs. Additionally, we employ an innovative model optimization technique to enhance our verification process. Our in-engine implementation of CTL model checking outperforms existing tools like NuSMV, even in more complex scenarios.