# Sequence Planner: A Framework for Control of Intelligent Automation Systems
## 2 The Sequence Planner Control Framework
### Operation Planner  
The operation planner (right part of Figure 8) is used to find a sequence of operations that should reach the goals of any currently active intentions. Currently, the planning engine in SP is based on nuXmv [25], which is a model checker rather than a classical planner. A model checker can prove temporal properties about a model by exploring the state space defined by a set of initial states and a set of transitions [26]. Temporal properties can be written in different ways, for example Computation Tree Logic (CTL) or Linear Temporal Logic (LTL) [27], which are both extensions to propositional logic. Such extensions include operators for expressing properties on past or future states. LTL has operators for the next state (operator **X**) that some formula should always (**G**) hold, that it should eventually hold (**F**), and that one formula should hold until another one does (**U**). For example, the formula \(\textbf{G}\)\((x\rightarrow\textbf{X}y)\) expresses that it is always the case that x implies y in the next state. In bounded model checking (BMC) [28], a reduction to Boolean satisfiability is performed with an upper bound on the number of transitions from the initial state that can be included. This allows for fast Boolean satisfiability (SAT) solvers to be used to find counterexamples. By letting the model checker try to prove that a future (desired) state is _not_ reachable, a counterexample, if found, can be used as a plan. This allows for the use of LTL specification that needs to be true for the duration of the plan. Consider the example of locking the door to secure the AGVs again. If both AGVs are outside the room, we want to give priority to \(r_{1}\) to enter the room first. However, if \(r_{2}\) is already in the room, it should not be forced to move out of the room just so \(r_{1}\) can enter first. We can express this operational specification using LTL in terms of the decision variables: \(r_{2}=outside\wedge\textbf{X}r_{2}=inside\implies r_{1}=inside\). The specification models with \(r_{2}\) transitioning from outside to inside imply that \(r_{1}\) is already inside. Figure 8: Overview of the planning system in SP. As seen in Figure 8, the transition runner continuously checks whether the goals of the currently executing intentions are reachable. This is performed by simulating the current plan against the current state. If the goals cannot be reached, or if the goals have changed, a new operation plan needs to be computed. A cache of plans is checked to see if this particular plan has already been computed before. If no plan is cached, a new BMC problem is generated, where the initial state is the current state of the system. A generated BMC problem and a minimal length counterexample for the example with the door and two robots can be seen in Listing 2. It includes the decision variables \(dl,r_{1},r_{2}\), and a transition relation which is generated from the operation definitions based on \(p_{j}\) and \(e_{j}\) for operation \(j\). The IVARs-s keep track of which transitions are taken in each step. An initial state is provided based on the current state of the automation system. Lastly, the goal is expressed as an LTL specification, where the LTL operator \(\mathbf{U}\) is used to specify that the formula \(\phi_{i}\) should hold until the goal is reached. The counterexample is a trace of which transitions were taken in order to violate the LTL specification (recall that the BMC problem is inverted).