/ltl-visualizer

An interactive visualizer for linear temporal logic (LTL)

Primary LanguageReScriptMozilla Public License 2.0MPL-2.0

Linear Temporal Logic Visualizer

✨ quickstrom.github.io/ltl-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.

Usage

The rough workflow for this little application goes as follows:

  1. Add formulae (see section on Syntax below)
  2. The atomic propositions in your formula are automatically shown above the formula
  3. Toggle the truth of an atomic proposition in each respective state (click the circles!)
  4. See how the truth of more complex formulae (e.g. with temporal operators) are affected when changing the atomic propositions
  5. (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!

Syntax

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:

A

This application uses (abuses, really!) the JavaScript parser in the browser to parse formulae. Thus, we use JavaScript function application syntax to form complex expressions, like those with operators.

Here's the temporal operator next applied to an atomic proposition:

next(A)

The logical connectives can't be || and && like in JavaScript, so they're called or and and:

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 (! in JavaScript) is called not:

not(A)

Logical implication is called implies:

implies(A, B)

The available temporal operators are:

  • next
  • eventually
  • always
  • until

The first three take one parameter, e.g. eventually(X). The until operator takes two parameters, like until(X, Y).

Sharing

The workspace state can be shared by clicking the blue "Share" button. On devices supporting native sharing, you'll get that dialog. As a fallback, the URL is copied to the clipboard.

As an example, here's a sharable URL: https://quickstrom.github.io/ltl-visualizer/?formulae=L%7CI%7CT&trace=%7C%7C%7C

Examples

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))

Hacking

  • Build: yarn build
  • Clean: yarn clean
  • Build & watch: yarn start

License

Mozilla Public License Version 2.0