Control and synthesis of open reactive systems

Abstract

This thesis studies the problem of automated synthesis of controllers and systems against formal specifications. The two central aims are to study these control problems for branching time specifications and to study them to achieve distributed control. The control synthesis problem for simulations and bisimulations are considered. It is shown that this could be solved in polynomial time. It is shown that how to automatically synthesize a polynomial state controller in polynomial time, whenever a controller exist. The control synthesis problem is studied for asynchronous simulations and shown that it is undecidable, and even the associated verification problem is undecidable in this setting. The undecidability results extend even to very simple classes of concurrent systems. The control and realizability problems for the branching time temporal logics CTL and CTL* are studied in two settings viz., in static and universal environment, and in reactive environment. The control problem for universal environments reduces to module checking and hence is for CTL and CTL* , EXPTIME-complete and 2EXPTIME-complete respectively. The complexities of these problems in reactive environments become exponentially harder. The control synthesis problem in distributed setting is investigated, where the process communicate with each other in a synchronous fashion and also interact with their local environments according to an architecture. For global specifications the only decidable architectures are the singly-flanked pipelines. The control problem for local specifications are studies and shown that the class of decidable architectures mildly increases. The exact class of architectures are characterized for which the control problem is decidable for local specifications, which is the class of architecture where each connected component is a sub architecture of a doubly flanked pipeline.