NBWMinimizer
Subproject |
S1 |
Categories |
Core algorithms, Model reduction |
Overview |
Non-deterministic Büchi automata (NBA) can efficiently represent properties in the formal methods context. For success of using them in model checking, they should be minimised prior to application. The NBWMiminizer tool is able to find smaller automata in many cases where classical bisimulation quotienting-based techniques fail. |
R. Ehlers and B. Finkbeiner. On the Virtue of Patience: Minimizing Büchi Automata. In Jaco van de Pol and Michael Weber, editors, 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), volume 6349 of Lecture Notes in Computer Science (LNCS), pages 129-145, 2010. |
|
Benchmarks |
See the experimental evaluation available here. |
Download |
|
Manual |
|
Status |
Prototype |