A two-phase approach for design of supervisory controllers for robot cells: model checking and Markov decision models

The supervisory controller for a robot cell 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 operating efficiency. We discuss modeling and control issues for robot task planning. We propose a two-phase approach to design the supervisory controller. 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, obedience to the technological operation sequence of each part, or prevention of buffer blockings. In the second phase, for performance design, we use semi-Markov decision models to determine the additional control decisions for which the controlled robot cell has the maximum throughput rate under the logical controller. We discuss the structure and algorithms of the performance control design problem