Anyone can understand temporal logic
if they have to save the realm

Benjamin Bisping

Tobias Loch

Mustafa Mohsen

Alessio N. Perna

Maximilian L. Stamm

University course

https://games.equiv.io/

LTL -> Game!

\(\sigma \vDash \varphi\)

• \(\langle \{B, R\}, \{Y\}, \{Y\}, \{B\} \rangle \vDash \bigcirc\bigcirc (Y \land \neg B)\)
• \(\langle \{B, R\}, \{Y\}, \{Y\}, \{B\} \rangle \vDash \Diamond B\)
• \(\langle \{B, R\}, \{Y\}, \{Y\}, \{B\} \rangle \not\vDash \Diamond (B \land Y)\)
• Game about building traces
  → Past formulas align more nicely with mechanics

Inspiration

[Slay the Spire, MegaCrit, 2019]

Demo

(play)

Flow

[Curtiss Murphy, 2016]

Logic landscape

Temporal
logics

modal­ities

traces

\(\omega\)-regular
languages

branching

 … 

Logics

logical
connectives

valua­tions

model
checking

complex­ities

 … 

Formal
languages

operator
nesting

formal
syntax

automata
theory

Chomsky
hierarchy

 … 

Discussion

Challenges:

• Infinite future in finite plays
• Ensure players engage with the formulas …

Opportunities:

• Trick players into learning temporal logic :D
• Mechanized science communication!

Try it!

• Game: https://benkeks.itch.io/tempus-fugit
• Code: https://github.com/benkeks/tempus-fugit

• Cheat: ↑ ↑ ↓ ↓ ← → ← → B A (“Konami code”)

Anyone can understand temporal logic

if they have to save the realm!