A new algorithm to solve synchronous FSM equations

Many problems over discrete event systems can be reduced to solving a synchronous FSM inequality A & X <= S or a synchronous FSM equation A & X = S, where X is a free variable and & is the synchronous composition operator. In this paper we address the problem of solving a multi-component FSM equation, We study the most general solution of a synchronous FSM equation defined over several FSMs. In particular, we show that a solvable equation has always a largest solution, then we consider the largest alphabet of actions over which a solution exists, from which it is possible to extract the largest solution over a restricted set of alphabets.