Algorithms for Solving FSM Equations: BALM - The Unknown Component Problem: Theory and Applications - page 78

Part II
Algorithms for Solving FSM Equations:
BALM

The first part of this topic presented the theory of language equations for syn-
chronous composition. The theory was developed with several objectives in mind:

• Generalize and unify several known approaches to solve the unknown component

problem within the framework of solving language equations.

• Provide a uniform method for expressing several classes of practical problems.

• Enable an efficient software implementation to explore the limits of practical

applications.

• Provide a platform on which new algorithms can be developed and tested.

In Part II, we focus on the efficient implementation aspects of this work. A software
system was developed, BALM, the Berkeley Automata and Language Manipulation
system, based on the multi-valued logic synthesis environment, MVSIS [46].
Both software packages and their documentation are available from the Download
Software link on the web site of the UC Berkeley MVSIS: Logic Synthesis and
Verification Group [52]. When implementing the theory, we had the following
objectives:

• To validate the theory as well as to refine it during its development when counter-
examples showed that some conjectures did not hold.
• To solve some practical problems by making the implementation as efficient as
possible.
• To facilitate instruction about finite automata, by developing a generic finite
automata calculator supported by the ability to graphically display example
results.
BALM utilizes the programming environment of MVSIS as much as possible. 1 The
implementation was organized as a set of modules to facilitate porting, reuse in other
applications, and ease of maintenance and extension. Multiple implementations of

1 An environment with multi-valued variables was chosen because such variables enable easier
specification of automata or FSMs and, at the same time, facilitate debugging.