DESCRIBING PROGRESSIVE SOLUTIONS TO A PARALLEL FSM EQUATION | Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics. 2008. № 1(1).

We consider the problemof deriving a component X that combined with the known part of system C, called the context, conforms to a given overallspecification S. Many problems of logic synthesis and analysis can be reduced to solving a parallel Finite State Machine (FSM)equationC ◊ X=S. However, not each solution to the equation is of practical use. In this paper, we are interested in progressivesolutions, i.e. solutions which have no livelocks without exit when composed with the context. We propose a novel algorithm forderiving a largest progressive solution by removing non-progressive strings from the largest solution to the equation. Since, ingeneral, the number of such strings is infinite, we show that a proposed algorithm terminates