Describing progressive solutions to a parallel FSM equation

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