RESOLUTION-BASED APPROACH TO COMPATIBILITY ANALYSIS OF INTERACTING AUTOMATA

The problem of compatibility analysis of two interacting automata aris es in the development of algorithms for reactive systems if partial no ndeterministic automata serve as models for both the reactive system a nd its environment. Intuitively, two interacting automata are compatib le if a signal from one automaton always induces a defined transition in the other. We present the method for solving this problem in the au tomated design of reactive system algorithms specified by formulas of a first-order monadic logic. Compatibility analysis is automatically p erformed both for initial specifications of the algorithm and its envi ronment and for any specification of the same kind obtained as a resul t of changes made by the designer. So, there is a need in the developm ent of methods for solving this problem at the level of logical specif ication. The methods based on the resolution principle proved to be ve ry helpful for this purpose.