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

Pnueli, Amir; Rosner, Roni

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.

MSC:

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

Keywords:

program derivation; program specification; concurrency; temporal logic; asynchronous reactive program; program synthesis by constructive theorem proving

Citations:

Zbl 0681.00016