Linear Temporal Logic Visualizer
This is an interactive visualizer for linear temporal logic (LTL), made as a companion tool for the article Specifying State Machines with Temporal Logic . Use this to play around with formulae and traces to get a better sense of how the temporal operators work.
The rough workflow for this little application goes as follows:
- Add formulae (see section on Syntax below)
- The atomic propositions in your formula are automatically shown above the formula
- Toggle the truth of an atomic proposition in each respective state (click the circles!)
- See how the truth of more complex formulae (e.g. with temporal operators) are affected when changing the atomic propositions
- (Repeat and learn LTL for great good!)
NOTE: The last state in the trace is considered repeating forever. We can't have an infinite number of checkboxes on a web page, but we want to mess around with infinite traces nonetheless!
The most basic syntactic construct is the atomic proposition. It's denoted by a single uppercase letter (A-Z), and it represents something that is true or false in a given state. Here's an atomic proposition:
Here's the temporal operator
next applied to an atomic proposition:
The logical connectives can't be
or(A, B) and(C, D)
Those operators are variadic, meaning that you can pass one or more arguments to them:
or(A, B, C, D)
Similarly, negation (
Logical implication is called
The available temporal operators are:
The first three take one parameter, e.g.
until operator takes two parameters, like
Here's a few valid formulae:
A implies(A, B) next(B) or(A, next(C)) always(A) until(A, or(B, C)) eventually(always(D))
- Build & watch: