Towards a computer-aided design of reactive systems

We consider a new approach to synthesize abstract machines for reactive programs that interact with processes in order to achieve some control requirements in the context of the Supervisory Control Theory. The motivation behind our synthesis approach is related to the problem of scalability. Generally, synthesis procedures are based on a comparison of two state spaces (fixpoint calculation-based approach) or an exploration of a state space (search-based approach). In neither case do the synthesis procedures scale to specifications of realistic size. To circumvent this problem, we propose: i) to combine two formal notations for the representation of reactive programs in addition to the one for specifying control requirements; and ii) to integrate a synthesis procedure in a framework in which various transformations are applied with the sole aim of solving a smaller control problem from an abstract model.