Bisimulation as a Service

Check behavioural equivalence of your models NOW!

What we do as BaaS

We provide an online service for bisimulation checking. Bisimulation is a must in the Industry 4.0 era. Correctness and robustness of your software products are our top priority. With BaaS, we are changing the way you do verification.

Developers can now check behavioural equivalence with the touch of a button, increasing their productivity. We support many types of bisimulation, including the latest up-to techniques.

You can register for a monthly subscription which allows you to check many models. We provide a free plan with reduced functionality.

What is a bisimulation?

Two systems are bisimilar if they match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.

A bisimulation relation is a certificate of this equivalence. Our service computes this certificate automatically for you. This makes our service trustworthy and secure, as it does not only return a binary output.

If your system contains a bug, our service will not be able to produce this certificate. Instead, it will return a counterexample, which can be used to resolve the bug.

Bisimulations are also used to minimise your state-based systems. This enables model-checkers to prove correctness in terms of temporal logics.


Our algorithms are state-of-the art, using up-to techniques, making us the most efficient BaaS. These up-to-techniques compress the bisimulation by using algebraic and coalgebraic properties of the system. It allows the bisimulation algorithm to exit early and find bugs more quickly. This is not only good for efficiency and throughput, it also shrinks the size of the certificate.

Prof. Dr. Rob van Glabbeek.


"BaaS is by far the most user-friendly bisimulation checker I have every tried. Small systems, or ones with millions of transitions, Baas gives me the right answers in virtually no time at all. Never again need I experiment with dotted lines on a whiteboard: just pipe it through BaaS and all will be clear!"

- Rob van Glabbeek

BaaS Plans

Get in touch to inquire about the pricing. Below is a table of the different features we provide.

You getFreePremium BaaS
Maximal number of models per month109000
Maximal number of states per model501000000
Maximal number of transitions per model1009000000
Standard (strong) bisimulation
Branching bisimulation
Bisimulation up-to transitive closure and congruence
Bisimulation up-to bisimulation
O(m log n) algorithms
Big Data Types
Deterministic Automata
Nondeterministic Automata
Weighted Automata
Weighted Tree Automata
Deterministic Register Automata
Markovian Timed Fault Trees
Quantum Software Product Line Systems
Labelled Transition Blockchain Coalgebras

Upon request, we can provide divergence-preserving branching bisimilarity for citizens from The Netherlands and France.


We're a team of bisimulation technologists and serious entrepreneurs. We work around the clock, to make sure your bisimulations are always ready to go.

Joshua Moerman, PhD.
Founder, Bisimulation Evangelist.

Jurriaan Rot, PhD.
CEO, CPO, and CTO.
Copyright 2020 - BaaS - Bisimulation Online