Information Technology Reference
In-Depth Information
is time-consuming and far from fail-proof: in some cases, gameplay bugs are
not immediately apparent to the human eye. In this setting, the use of runtime
verification techniques presents the potential for improving the gameplay bug
harvesting step. However, video games rely a lot on fast player inputs and are
much more sensitive to speed and timing than traditional software; it is there-
fore important that the use of a monitor does not slow down the game in any
noticeable way. This paper presents early results on this approach and illustrates
how gameplay bugs of a popular platform game,
Infinite Super Mario Bros.
,can
be specified as temporal logic formulæ and eciently caught at runtime using
an off-the-shelf monitor.
2 Gameplay as Temporal Logic Constraints
As opposed to most standard software, video games are not entirely driven by the
user. Most games include a physics engine and a form of artificial intelligence to
update the game environment even in the absence of any input from the player.
Moreover, these updates must be executed a minimum of 30 times (called
frames
)
per second, with 60 frames per second (fps) being a reasonable target for quality
animation. Noticeable disruptions of the frame rate are regarded by players as
bugs and have in the past caused the demise of some video game titles. This
concept is best exemplified by a well-known game called
Infinite Mario Bros.
(Figure 1), an open-source reimplementation of the popular platform game
Super
Mario World
, where various enemies and other game objects move around the
game area independently of the player's (i.e. Mario's) actions.
Infinite Mario is made of 6,500 lines of Java code and is available online.
1
It
is notable for being the subject of many research works on game testing and
applications of Artificial Intelligence algorithms in the past [5]. It has recently
been used as a testbed for the automated application of condition-action rules
aimed at correcting erroneous game states [7]. A similar approach has been
applied to
FreeCol
, a free version of the strategy game
Civilization
[4].
In the following, we push the concept further and attempt to formalize the
expected behaviour of various game objects as temporal logic constraints. In this
context, events represent various changes of state, both of the player's character
and of the surrounding enemies and objects. Each event is represented as a list
of parameter-value pairs, and has a parameter called
name
, indicating the type of
the event (e.g. Jump, Stomp, EnemyDead, etc.). The number and name of the
remaining parameters may differ depending on the event's type. For example,
when Mario stomps on an enemy, the unique ID of that enemy will be included
in the event; when Mario jumps, the height of the jump will be recorded.
The rules used to express the properties to monitor are represented with LTL-
FO
+
, an extension of Linear Temporal Logic (LTL). For example, the following
expression indicates that globally, if an enemy gets hit by a fireball that Mario
