In space exploration, robots are important to do some hazardous jobs instead of human. The robots usually work in an unstructured environment to operate non-cooperative targets. There are unpredictable events which can reduce the capacity of robots. And unfortunately the communication channel between robots and ground command center has limited band-width and high latency. Therefore, space robot system needs plans that can autonomously deal with unpredictable events. Executable plans must satisfy some well defined conventions. This paper proposes a formal representation of plan library based on Petri net as well as the way to define conventions based on LTL. The formal representation formalizes concepts such as event, action and behavior. And plan is a behavior instance. This approach could be used to generate rational plans automatically or with a litter help of human. We illustrate them with a space robot application example. © 2014 SERSC.