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.

Publications

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

See react.cs.uni-saarland.de/tools/nbwminimizer/

Manual

See react.cs.uni-saarland.de/tools/nbwminimizer/

Status

Prototype