What we do as BaaS
We provide an online service for bisimulation checking. 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.
Efficient
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.
Testimonials
Todo. Lorem Ipsum is slechts een proeftekst uit het drukkerij- en zetterijwezen. Lorem Ipsum is de standaard proeftekst in deze bedrijfstak sinds de 16e eeuw, toen een onbekende drukker een zethaak met letters nam en ze door elkaar husselde om een font-catalogus te maken. Het heeft niet alleen vijf eeuwen overleefd maar is ook, vrijwel onveranderd, overgenomen in elektronische letterzetting.
BaaS Plans
Get in touch to inquire about the pricing. Below is a table of the different features we provide.
| You get | Free | Premium BaaS |
|---|---|---|
| Maximal number of models per month | 10 | 9000 |
| Maximal number of states per model | 50 | 1000000 |
| Maximal number of transitions per model | 100 | 9000000 |
| Features | ||
| Standard (strong) bisimulation | ✓ | ✓ |
| Branching bisimulation | ✓ | |
| Bisimulation up-to transitive closure and congruence | ✓ | |
| Bisimulation up-to bisimulation | ✓ | |
| CEGAR & CEGIS API | ✓ | |
| O(m log n) algorithms | ✓ | |
| Big Data Types | ✓ | |
| Models | ||
| Deterministic Automata | ✓ | ✓ |
| Nondeterministic Automata | ✓ | |
| Weighted Automata | ✓ | ✓ |
| Weighted Tree Automata | ✓ | |
| Deterministic Register Automata | ✓ | |
| Quantum Software Product Line Systems | ✓ | |
| Labelled Transition Blockchain Coalgebras | ✓ |
Team
A CEO, some developers, some designers, etc. All of them have a PhD in related fields, etc. "Bisimulation evangelist."