Sequential synthesis by language equation solving
Nina Vladimirovna Yevtushenko, Tiziano Villa, Robert K. Brayton, Alexandre Petrenko, Alberto Luigi Sangiovanni-Vincentelli · 2003
Consider the problem of designing a component that combined with a known part of a system, called the context, conforms to a given overall specification. This question arises in several applications ranging from logic synthesis to the design of discrete controllers. We cast the problem as solving abstract equations over languages and study the most general solutions under the synchronous and parallel composition operators. We also specialize such language equations to languages associated with important classes of automata used for modeling systems, e.g., regular languages as counterparts of finite automata, FSM languages as counterparts of FSMs. Thus we can operate algorithmically on those languages through their automata and study how to solve effectively their language equations. We investigate the maximal subsets of solutions closed with respect to various language properties. In particular, we investigate classes of the largest compositional solutions (defined by properties exhibited by the composition of the solution and of the context). We provide the first algorithm to compute the largest compositionally progressive solution of synchronous equations. This approach unifies in a seamless frame previously reported techniques. As an application we solve the classical problem of synthesizing a converter between a mismatched pair of protocols, using their specifications, as well as those of the channel and of the required service. 1