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. +
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. +
+ Prof. Dr. Rob van Glabbeek.
+ Expert. +
Testimonial
+"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 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 | ✓ + | |
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. +
Team
+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. +