• Examples
  • Textual Definition
  • Transitions as CSV
  • SVG Picture
  • PhD Thesis: Generalized Equivalence Checking of Concurrent Programs
  • Paper: Process Equivalence Problems as Energy Games (CAV 2023)
  • Paper: One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics (EXPRESS/SOS 2024)
  • Source code (Scala.js)
  • About the LTBT Spectroscope

About the Linear-time–Branching-time Spectroscope

This is a tool for finding the best ways of distinguishing finite process models.

For the theoretical background, check out Bisping (2025): Generalized Equivalence Checking of Concurrent Programs

The LTBT Spectroscope is developed at MTV TU Berlin by:

  • Benjamin Bisping (benjamin.bisping@tu-berlin.de)