Modelling Asynchrony with a Synchronous Model.

The I/O Automaton paradigm of Lynch and Tuttle models asynchrony through an interleaving parallel composition and generalizes more comon interleaving models based upon message-passing, such as Hoare's CSP. It is not generally recognized that such interleaving models in fact can be viewed as special cases of synchronous parallel composition, in which components all move in lock-step. Let A be any set of finite-state I/O Automata drawing actions from a fixed finite set containing a subset DELTA. In this article we establish a translation T: A -> P to a class of omega-automata P closed under a synchronous parallel composition, for which T is monotonic with respect to implementation relative to DELTA, and linear with respect to composition. Thus, for A sup 1,...,A sup m, B sup 1,...,B sup n epsilon A and A=A sup 1 ||...||A sup m,B=B sup 1 ||...||B sup n, if DELTA is the set of actions common to both A and B, then A implements B (in the sense of I/O Automata) if and only if the omega-automaton language containment L(T(A sup 1) x...xT(Asup m)) subset L(T(B sup 1) x...xT(B sup n)) obtains, where || denotes the interleaving parallel composition on A and x denotes the synchronous parallel composition on P. For the class P, we use the L-process and model of omega-automata. This result enables one to verify systems specified by I/O Automata through model-checkers such as COSPAN or SMV, that operate on models with synchronous parallel composition. The translation technique generalizes to other interleaving models, although in each case, the translation map must match the specific model.