Solving inequalities over finite state machines in the reactive systems design

The problem of solving inequalities over finite state machines (FSMs) is considered. This problem arises in compositional approach to the design of reactive systems. The problem is formulated and solved at the level of FSMs specifications in the logical language $L$. We show how to compute the maximal solution to the inequality with respect to the operation of synchronous composition of FSMs.