On the synthesis of an asynchronous reactive module. (English) Zbl 0686.68015

Automata, languages and programming, Proc. 16th Int. Colloq., Stresa/Italy 1989, Lect. Notes Comput. Sci. 372, 652-671 (1989).
Summary: [For the entire collection see Zbl 0681.00016.]
We consider the synthesis of a reactive asynchronous module which communicates with its environment via the shared input variable x and the shared output variable y, assuming that the module is specified by the linear temporal formula \(\phi\) (x,y). We derive from \(\phi\) (x,y) another linear formula \(\chi\) (r,w,x,y), with the additional scheduling variables r, w, and show that there exists a program satisfying \(\phi\) iff the branching time formula (\(\forall r,w,x)(\exists y)A\chi (r,w,x,y)\) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm, of doubly exponential time and space complexity, for constructing a program that implements the specification whenever it is implementable. In addition, we provide some matching lower bounds.


68Q60 Specification and verification (program logics, model checking, etc.)
68N25 Theory of operating systems
03B45 Modal logic (including the logic of norms)
68Q25 Analysis of algorithms and problem complexity


Zbl 0681.00016