DBA Minimizer
Subproject |
S1 |
Categories |
Core algorithms, Model reduction |
Overview |
Deterministic Büchi automata (DBA) can be used to model most properties found in the specification of circuits in practice. While the class of languages representable by DBA does not include for example all properties representable by linear-time temporal logic (LTL), in contrast to non-deterministic Büchi automata, they have an important advantage: the problem of deciding whether an automaton is minimal is contained in the complexity class NP. Hence, for the minimization of these automata, SAT solvers can be used. The DBA Minimizer tool set uses an external SAT solver to perform such a minimization task. It contains tools for encoding the state space reduction problem into a DIMACS SAT instance and interpreting a satisfying assignment back to a smaller DBA. An included python script encapsulates all steps. |
R. Ehlers. Minimising Deterministic Büchi Automata Precisely using SAT Solving. In O. Strichman and S. Szeider, editors, 13th Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of Lecture Notes in Computer Science (LNCS), pages 326-332, 2010. |
|
Benchmarks |
See the experimental evaluation available here. |
Download |
|
Manual |
|
Status |
Prototype |