George J. Pappas, Graduate Student
(Professor S. Shankar Sastry)
Verification of reactive modules [1] is the analysis process where a given module is verified to satisfy a desired specification. In this work, we consider the inverse problem where given a module called Plant and a desired specification on the Plant, we ask whether there exists a module called Controller such that the parallel composition of the Plant with the Controller satisfies the desired specification. If such a Controller exists the Plant is called controllable and automatic Controller synthesis is performed whereas if such a Controller does not exist then the Plant is called uncontrollable and no Controller design will satisfy the specification.
(No figures supplied)