Control and synthesis of open reactive systems

DSpace/Manakin Repository

Control and synthesis of open reactive systems

Show full item record

Title: Control and synthesis of open reactive systems
Author: Madhusudan, P.
Advisor: Ramanujam, R.
Degree: Ph.D
Main Subjects: Computer Science
Institution: University of Madras
Year: 2001
Pages: v; 155p.
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.
URI: http://hdl.handle.net/123456789/95

Files in this item

Files Size Format View
UNMTH70.pdf 911.0Kb PDF View/Open

This item appears in the following Collection(s)

Show full item record

Search DSpace


Advanced Search

Browse

My Account