BALM-II

BALM: Finite-state automata and their languages are well-studied subjects since the early development of computation theory. Traditional automata manipulations are based on explicit state representation, and are limited to automata with a few thousand states. The manipulation of automata became more practical with the advent of efficient symbolic techniques based on binary decision diagrams (BDDs), satisfiability (SAT) solvers and AND-INVERTER graphs (AIGs). Based on these techniques, the BALM (Berkeley Automata and Language Manipulation) package aims at providing an experimental environment for efficient manipulation of finite automata in various application domains, e.g., synthesis, verification, control, etc. The environment features the most typical automata operations, such as determinization and state minimization, as well as some visualization capabilities, which rely on the powerful graph visualization software [Graphviz]. The applicability of BALM to finite-state machine synthesis is demonstrated by solving an unknown component problem formulated using language equations.