Applying Symbolic Model Checking to Node-graph Style Game Scripts with Time Constraints
Ryugo Tanaka, Tomoyuki Yokogawa, Sousuke Amasaki, Hirohisa Aman, Kazutami Arimoto · 2023
In our previous work, we proposed a method to convert a game program created in UE5 Blueprint into an input model for the model-checker nuXmv to achieve automatic verification. This framework enables the automatic generation of models by formally defining the semantics of nodes. In this paper, we extend this method to handle the nodes with time constraints. To achieve this, we additionally define a global clock as a variable that represents the time elapsed since the start of the script.