Application name:

Control Logic Design of Robot Work Cells

Organisation:

Department of Industrial Engineering, KAIST (Korea Advanced Institute of Science and Technology), Taejon, Korea.

Method:

Our Two-Phase Method: (1) use of CTL-based or automata-based model checking for Logical Proof (Logical Controller), and (2) use of Markov Decision Model and Algorithms for Performance Optimization (Performance Controller).

Tools:

SMV (from Carnegie Mellon University), and COSPAN (from AT&T).

Domain:

Robotics, Supervisory Control of Automated Manufacturing Systems.

Period:

1995 - 1997

Size:

300-1000 lines of specification, 1 man-month for each project.

Description:

We aimed at design of supervisory control logic of automated manufacturing systems (AMT) like robotic workcells. We proposed a two-phase method for controller design, the logical controller design and the performance controller design. For logical controller design, we propose the use of formal model checking methods (like SMV or COSPAN) to verify the plant controlled by a logical controller against the control specifications. For performance controller design, we used Markov decision models to find an optimal control rule that minimizes the cycle time for the plant controlled by the logical controller. We focused on robot task level modeling. Once the robot task sequence is determined, the detailed action of robots, machines, or other equipment can be subsequently determined. The plant was modeled in concurrent automata. The logical control requirements are specified in computational temporal logic or automata. We applied our methods for three machine robot cells processing multiple parts, a three-robot machining and assembly work cell, and a two-robot assembly cell.

Conclusions:

Our methods were successful. Model checking took only a few seconds and the value iteration algorithm for MDP models efficiently finds a robust solution, which dominate other heuristic rules even for non-Markovian (having non-exponentially distributed times) situations.

Publications:

Tae-Eog Lee and Jin-Whan Lee: "A Two-Phase Approach for Design of Supervisory Controllers for Robot Cells: Model Checking and Markov Decision Models". Proceedings of the 5th IEEE International Conference on Emerging Technologies and Factory Automation, pp.56-62, November 1996 (the full version will appear at Annals of Operations Research, 1997).

Tae-Eog Lee, Jin-Kyu Lee, and Jin-Whan Lee: "Supervisory Controller Design of Robot Assembly Cells by Model Checking Techniques". Proceedings of the 20th International Conference on Computer and Industrial Engineering, pp.129-132, October 1996.

Jae-Man Jeong: "Design of Supervisory Control Logic of a Multi-Robot Assembly Cell by Automata-Based Model Checking and Markov Decision Models". Master Thesis, Department of Industrial Engineering, KAIST (a proceeding version will appear at Korean IE/MS Joint Conference, April 1997).

Contact:

Name:	Tae-Eog Lee, Associate Professor
Organisation:	Department of Industrial Engineering
Address:	KAIST 373-1 Gusung-dong, Yusung-ku Taejon 305-701,
Country:	Korea (South)
Phone number:	+82 (42) 8693122
Fax:	+82 (42) 8693110
E-mail:	telee@sorak.kaist.ac.kr
Personal website:	http://ie1.kaist.ac.kr/~yhshin/profs.html

URL:

http://ie1.kaist.ac.kr/~yhshin/profs.html

Remarks:

We wish to apply our engineering methods for more diverse, realistic control problems for automated manufacturing systems or other domains. We are working on development of a tool set that automates our design process and on implementation of designed controllers for PLCs or PCs in distributed environment.

© copyright 2004 | Formal Methods Europe