Tempus fugit: Anyone can understand temporal logic if they have to save the realm
2026-07-06 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors created a simple browser game called 'Tempus fugit' where players act as magicians fighting enemies by casting spells. To win, players must understand and use special logic formulas called linear temporal logic with past, which depend on events happening over time during the game. The paper explains how the game's design helps players learn these complex logic ideas by making them part of the gameplay. This approach aims to make formal logic less intimidating by turning it into a fun, interactive experience.
linear temporal logicformal logicfinite tracespast operatorsgame mechanicslogic formulasinteractive learningbrowser gametemporal logiceducational games
Authors
Benjamin Bisping, Tobias Loch, Mustafa Mohsen, Alessio Nicolo Perna, Maximilian Lukas Stamm
Abstract
Often, the easiest way to learn something is to have to use it for a purpose. This purpose can be playful: In 'Tempus fugit', the player takes on the role of a magician who has to defeat enemies by casting spells. The applicability of spells and enemy attacks depends on the truth of formulas in linear temporal logic with past with respect to a trace that the player gradually builds. So, whoever wants to save the realm from monsters has to learn to read logic formulas. This paper describes the small browser game and explains our design choices. We expose how game mechanics connect to linear temporal logic with past over finite traces, and how this can help players approach a daunting topic like formal logic.