We discuss a two-phase approach to supervisory controller design problems for robot workcells. The supervisory controller is specified as a dynamic control policy that determines the part processing sequence and the robot work cycle depending on the state of the cell. The supervisory controller should be designed not only to satisfy the prescribed logical requirements or constraints but also to achieve the maximum efficiency. In the first phase, for logical design, we use a model checking technique for concurrent automata to verify whether the proposed logical control rules satisfy the logical requirements. The logical control requirements may include deadlock prevention, the technological operation sequence of each part, or prevention of buffer blockings. We model the robot cell plant and the proposed supervisory controller as a network of automata. The logical control requirements are specified using a branching time logic called computation tree logic (CTL). To verify the supervisory control logic against the logical control requirements, we use a model checking tool called SMV (Symbolic Model Verifier) that has been proven to successfully solve very large verification problems for concurrent automata. SMV checks violations of the controlled plant and generates counterexamples. An iterative process of model checking induces less restrictive, that is, more permissible, controllers that conforms to the control requirements. The plant that is controlled by such a permissible controller has nondeterministic behavior and requires further control decisions to be a complete controller. Therefore, in the second phase, for performance design, we use Markov decision models to determine the additional control decisions for which the controlled robot cell has the minimum cycle time. Thus, by the model checking approach and Markov decision models, we can develop more compliant and efficient supervisory controllers for complex robot workcells.
