Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time

Linear-Time–Branching-Time Spectroscope

The “Linear-time–Branching-time Spectroscope” is a web app to find all preorders, equivalences and inequivalences from the (strong) linear-time–branching-time spectrum for small processes as described in Bisping, Jansen, Nestmann, LMCS 2022.

It runs online on .

Just input CCS-style processes, give the two processes you want to compare with @compare "P1,P2" and click on the gutter next to the compare-statement!

To explore possible minimizations of the system, write @minimize and click on the gutter!

It's also possible to enter processes with internal behavior, either by tau.P actions or due to communication, (a.0 | a!0) \ {a}. To compare with respect to the weak spectrum, use @compareSilent "P1,P2".

How to build

The project can be built using sbt by.

sbt webStage

This will download all dependencies and output a website under web/target/web/stage/index.html that can be run locally in any modern browser.

In order to test that the algorithm determines the expected (in-)equivaences for the example processes from, run:

sbt "shared/test"

To perform benchmarks, run:

sbt "shared/run benchmark"

Docker image

To build a docker image that bundles the Scala dependencies and the fiddle (and export it to tgz), run:

docker build . -t equivalence-fiddle
docker save equivalence-fiddle | gzip > doc/artifact/equivalence-fiddle-docker.tar.gz

By default, the docker image starts up a small webserver serving the fiddle on 8080, which can be made live on like this:

docker run -p --name equivalence-fiddle -d equivalence-fiddle

To reproduce benchmarks from the container, you then can (for instance) run:

docker exec -it equivalence-fiddle sbt "shared/run benchmark"

Theoretical background

The algorithm uses a generalization of the bisimulation game to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. Using these, we can give a precise characterization of how much distinguishing power is needed to tell two processes apart—and thus also determine the best fit of equivalences to equate them.

Developed by

The LTBT Spectroscope is developed at MTV TU Berlin by Benjamin Bisping (

The code is subject to the MIT License to be found in LICENSE. The full source can be obtained from and via DOI.