Temporal Logic: The Master Plan

DASHBOARD

MISSION CONTROL

Your bridge between abstract theory and formal mastery.

TOTAL XP

3 480

+320 this week

⚡

LESSONS DONE

14 / 22

Basics complete

🧪

BEST COMBO

x12

Time Attack record

🔥

MASTERY BY OPERATOR

Next (X)

90%

Eventually (F)

75%

Globally (G)

68%

Until (U)

40%

Release (R)

22%

CONTINUE MISSION

Pick up where you left off.

✅ Lesson 3 — Eventually (F) DONE

▶️ Lesson 4 — Until (U) RESUME

🔒 Challenge — Advanced Kripke LOCKED

LEARN — BASICS

DIFFICULTY: EASY

Guided micro-lessons on basic Kripke structures. +50 XP per correct check.

LESSON PLAYER

📚 LESSON 1 — WHAT IS A STATE?

A Kripke structure is states joined by transitions. Each state is labelled with the atomic propositions true there.

S0 : { p, q }

QUICK CHECK

Which propositions hold in S0?

A p and q ✔

B only p

C nothing is true

📚 LESSON 2 — TRANSITIONS

Arrows show how the system moves between states over time. A path is an execution (a trace).

S0 → S1 → S2 → S3

QUICK CHECK

What does S0 → S1 mean?

A S0 equals S1

B step from S0 to S1 ✔

C S1 before S0

📚 LESSON 3 — EVENTUALLY (F)

F q = "eventually q": somewhere on the path, q becomes true.

S0 → S1 → S2(q) → S3

QUICK CHECK

F q holds if q never occurs?

A yes, always

B no — needs q at some point ✔

C only at first state

MODULE PROGRESS

✅ What is a state? +50 XP

✅ Transitions +50 XP

▶️ Eventually (F) CURRENT

🔒 Globally (G) LOCKED

🔒 Until (U) LOCKED

Basics

64%

CHALLENGE

MEDIUM → ADVANCED

Draw a structure or write a formula. Immediate feedback. +150 XP.

VERIFY THE STRUCTURE

Target formula

G (p → F q)

Your answer — write a formula

✔ PASS — example correct response.
Formula G (p → F q) holds: on every path, whenever p is true, q eventually follows. +150 XP awarded.

✘ FAIL — example incorrect response & hint.
Counter-example: S0(p) → S3 → S3 → ... — p holds at S0 but q never returns, breaking "eventually q". Hint: inspect the self-loop on S3.

Build a structure that satisfies G (p → F q). Tools below are live.

How to use

➕ STATE — click empty space to place a state.
→ TRANSITION — click source, then target (same node = self-loop).
TOGGLE p / q — click a state to add/remove that label.
◎ ACCEPTING — click a state to mark it accepting (double circle).
🗑️ DELETE — click a state to remove it.
✋ DRAG — grab any state to reposition it.

TIME ATTACK

RAPID FIRE

Beat the clock. Combos multiply XP. One wrong answer ends the run.

00:38

COMBO x4 🔥

SCORE

1 250

🔥 DRAW IT: build a Kripke structure that satisfies F (p ∧ X q)

Objective

Draw a model where, somewhere on a path, p holds and the next state has q. That makes F (p ∧ X q) true.

SKILL TREE

PROGRESSION MAP

Unlock operators in order. Each node needs the previous mastered.

✅ STATES

S : {p,q}

Mastered

✅ NEXT (X)

X p

Mastered

✅ EVENTUALLY (F)

F q

Mastered

▶️ UNTIL (U)

p U q

In progress · 40%

🔒 GLOBALLY (G)

G p

Locked

🔒 RELEASE (R)

p R q

Locked

🔒 NESTED

G(p → F q)

Locked

ACHIEVEMENTS

12 / 30 UNLOCKED

Earn badges for milestones and combos.

🏆

FIRST TRACE

Completed lesson 1

⚡

10-COMBO

Time Attack x10

🧪

BASICS DONE

All basics cleared

🔥

7-DAY STREAK

One week strong

🔒

UNTIL MASTER

Master the U operator

🔒

RELEASE ADEPT

Master the R operator

🔒

NESTED NINJA

Solve a nested formula

🔒

NO-HINT RUN

Time Attack, zero hints

LEADERBOARD

COS700 COHORT

Ranked by total XP · optional gamification extension (mock-up data).

👑

RANK #1 · ORACLE TIER

Prof. Timm

Supervisor · flawless nested-formula streak · 100% operator mastery

12 840

TOTAL XP

Lv 42

RANK

x24

BEST COMBO

21

DAY STREAK

🥈

#2 SILVER

LU

Linus Ungerer

8 920 XP

Lv 14 · Navigator · 12-day streak

🥇

#1 CHAMPION

PT

Prof. Timm

12 840 XP

Lv 42 · Oracle · 21-day streak

🥉

#3 BRONZE

LS

Lukas Swanepoel

6 540 XP

Lv 11 · Pathfinder · 9-day streak

COHORT STANDINGS

Full ranking for the educational-software honours group.

01

PT

Prof. Timm

Supervisor · Oracle tier

12 840

TOTAL XP

CHAMPION

02

LU

Linus Ungerer

Navigator · 18 / 22 lessons

8 920

TOTAL XP

SILVER

03

LS

Lukas Swanepoel

Pathfinder · Until (U) mastered

6 540

TOTAL XP

BRONZE

04

RN

Ruan Nel

Cadet · you · 14 / 22 lessons

3 480

TOTAL XP

YOU

OPTIONAL EXTENSION · MOCK DATA ONLY · NOT PART OF THE MINIMAL VIABLE TOOL

SETTINGS

PREFERENCES

Theme, notation, and accessibility options.

ThemeDark · Space

LTL notationSymbols (G F X U R)

Sound FXOn

Reduced motionOff