Abstract:
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.
Keywords:reactive system, language $L$ specification, $\Sigma$-automaton, synchronous composition of $\Sigma$-automata, inequality over $\Sigma$-automata, maximal solution.
Fulltext:
PDF file (584 kB)