RESOLUTION-BASED APPROACH TO COMPATIBILITY ANALYSIS OF INTERACTING AUTOMATA

Citation
An. Chebotarev et Mk. Morokhovets, RESOLUTION-BASED APPROACH TO COMPATIBILITY ANALYSIS OF INTERACTING AUTOMATA, Theoretical computer science, 194(1-2), 1998, pp. 183-205
Citations number
15
Categorie Soggetti
Computer Science Theory & Methods","Computer Science Theory & Methods
ISSN journal
03043975
Volume
194
Issue
1-2
Year of publication
1998
Pages
183 - 205
Database
ISI
SICI code
0304-3975(1998)194:1-2<183:RATCAO>2.0.ZU;2-U
Abstract
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.