Tempus fugit: Anyone can understand temporal logic if they have to save the realm
Source: arXiv:2607.05062 · Published 2026-07-06 · By Benjamin Bisping, Tobias Loch, Mustafa Mohsen, Alessio Nicolo Perna, Maximilian Lukas Stamm
TL;DR
Tempus fugit addresses the challenge of making formal temporal logic accessible and engaging to learners without prior background by embedding it into a browser-based single-player game. The player acts as a magician who must strategically manipulate a temporal trace of atomic propositions to cast spells and defeat enemies. The game mechanics link directly to linear temporal logic with past (PLTL) formulas over finite traces, allowing players to learn logic semantics implicitly while playing. Key innovations include embedding PLTL formulas in spell applicability and enemy conditions, a visual temporal trace interface, and gradual introduction of logical operators through escalating levels.
The paper details the game’s design, pedagogical rationale, and implementation, emphasizing how formal notation is gamified and integrated into narrative and mechanics. The authors highlight how players experience temporal operators in an intuitive spatial-temporal visualization, slowly build fluency without explicit didactic instruction, and are incentivized naturally to master the logic for game success. While limited as a standalone educational tool, Tempus fugit is positioned as an engaging first step that could complement formal logic education or science communication.
Key findings
- Tempus fugit introduces temporal logic with past (PLTL) to non-expert players through gameplay mechanics requiring manipulation of atomic proposition valuations over time.
- Players build a finite temporal trace incrementally, editing only the current time step, to satisfy or falsify PLTL formula conditions on spell cards and enemy attacks.
- Levels escalate in complexity: starting with propositional logic only, then adding past modalities (previous, once, historically) and finally future operators (next, globally, eventually).
- The game interface visualizes traces as a table of rune valuations over time, concretely linking formulas to their temporal semantics in real-time.
- Players must learn to read and interpret standard PLTL notation with only an optional help screen that provides examples but no direct formula explanations.
- Game progression and success naturally incentivize comprehension: understanding more formulas enables winning harder battles, though failure to understand does not block basic progress.
- The implementation uses a TypeScript browser client with a custom event-driven PLTL parser/interpreter, enabling accessibility without installation and offline play after loading.
- Embedded narrative and magical theme help reframe formal logic notation from arcane and intimidating to an immersive, purposeful language users must master.
Threat model
n/a - the work is focused on educational game design to teach temporal logic rather than adversarial security scenarios or threat mitigation.
Methodology — deep read
The methodology centers on designing, developing, and deploying a browser-based game to scaffold learning of linear temporal logic with past (PLTL). The adversary is the game environment itself, which challenges the player to meet logical conditions encoded as PLTL formulas to cast spells and survive enemy waves. No external adversaries or attackers are considered. The main assumption is that players have no prior logic knowledge but can learn via experimentation and immersion.
Data consists of the game state, represented as a finite trace σ of atomic proposition valuations over discrete time steps (turns). Atomic propositions correspond to four colored runes manipulated by the player each turn. The trace grows incrementally each turn, with the player able to flip the valuation of up to two runes at the current time step. PLTL formulas on cards and enemies provide applicability conditions evaluated on this trace.
The core algorithm is a PLTL formula parser and interpreter implemented using modified shunting-yard parsing to convert infix notation to postfix and then abstract syntax trees. The interpreter evaluates formulas on the finite trace semantics of PLTL as per definitions in the paper. Formulas include propositional operators, past modalities (previous, once, historically, since), and some future operators (next, globally, eventually), though until/since are supported but not used currently. Evaluation ensures formula truth at the current time step dictates card/enemy effect applicability.
Training of the player is guided by gradual level design rather than machine training. Levels start with propositional logic formulas only, then progressively introduce past and future temporal operators with increasing nesting complexity. The game mechanics encourage the player to explore the space of rune valuations and formula truth.
Evaluation is qualitative/experiential: success in levels demonstrates implicit learning; no formal user studies or metrics reported. The game design uses scaffolding (help screens, incremental complexity) and narrative immersion to evaluate usefulness as a learning machine. Code is open-source on GitHub, supporting reproducibility of implementation but no formal datasets or models exist.
A typical game session advances turn by turn: The player draws cards with PLTL conditions, adjusts rune valuations, attempts to meet formula conditions to cast spells, battles enemies whose own attacks have formula conditions, and builds the trace over time, witnessing how temporal logic operators affect game outcomes viscerally.
This implementation and design approach clarifies key temporal logic concepts and syntax in a playful, accessible way, though no formal learning assessment was conducted. The source code availability and browser platform maximize accessibility and reproducibility of the tool itself.
Technical innovations
- Embedding PLTL formulas with past and future modalities as card and enemy attack conditions directly affecting gameplay applicability.
- Incremental finite trace building with player-controlled atomic proposition valuations visualized as a spatio-temporal matrix to concretize temporal operators.
- Event-driven architecture decoupling state changes in the game with a custom PLTL interpreter parsing infix formulas into abstract syntax trees for evaluation.
- Semantic scaffolding by stepwise introducing logical operators and gating game complexity on player increasing formula comprehension.
- Narrative integration of temporal logic notation into magic-themed game lore as an immersion and motivation technique.
Datasets
- Tempus fugit game state traces — finite incremental sequences of atomic proposition valuations — internal to gameplay
Figures from the paper
Figures are reproduced from the source paper for academic discussion. Original copyright: the paper authors. See arXiv:2607.05062.
Fig 1: Main game scene of Tempus fugit in level 6 “What worm is this?” with the player about
Fig 2: Help screen describing the once modality.
Fig 3: Deck builder combining “Lightning rain” with cards that benefit from global light
Limitations
- No formal user study or empirical evaluation of learning outcomes or retention beyond anecdotal observations.
- Limited coverage of temporal logic: until and since modalities are implemented but not used in gameplay.
- Game only facilitates initial exposure and basic comprehension; deeper mastery requires supplemental formal instruction.
- Interface lacks direct formula semantic explanation on cards, relying on player to consult help screens or infer meaning.
- Screen layout not optimized for mobile devices, limiting accessibility on smaller screens.
- Finite-trace semantics differ from classical infinite-trace LTL, which may limit direct transfer to some formal verification contexts.
Open questions / follow-ons
- How effective is gameplay in improving temporal logic literacy compared to traditional teaching methods? Empirical user studies needed.
- Can additional automated feedback or visualization tools within the game improve formula understanding and accelerate learning?
- How to extend gameplay mechanics to cover deeper and more expressive temporal logics (e.g., until/since, branching time)?
- What is the transferability of learned PLTL comprehension from the game context to formal verification or programming tasks?
Why it matters for bot defense
Tempus fugit offers a novel approach for CAPTCHAs and bot defense engineers interested in leveraging formal logic as a human challenge. Its methodology of embedding non-trivial logical formula interpretation within a game context demonstrates how complex reasoning tasks can be made engaging and learnable. This approach could inspire new CAPTCHAs that require understanding temporal relationships or logical formula evaluation over interaction histories, raising the difficulty for automated bots.
However, the game is designed primarily for educational purposes rather than real-time bot detection or denial-of-service resilience. Practitioners should note the trade-offs in complexity, user friction, and accessibility. Simplified versions or modular components of Tempus fugit’s PLTL interpreter and trace visualizations may underpin novel logic-based challenge tasks. The emphasis on gradual scaffolding and integrating logic into natural mechanics is particularly relevant to designing CAPTCHAs that aim for learnability and fairness, not mere obfuscation.
Cite
@article{arxiv2607_05062,
title={ Tempus fugit: Anyone can understand temporal logic if they have to save the realm },
author={ Benjamin Bisping and Tobias Loch and Mustafa Mohsen and Alessio Nicolo Perna and Maximilian Lukas Stamm },
journal={arXiv preprint arXiv:2607.05062},
year={ 2026 },
url={https://arxiv.org/abs/2607.05062}
}