# Sequence Planner: A Framework for Control of Intelligent Automation Systems
## 2 The Sequence Planner Control Framework
### Resource Specifications  
Formal specifications can be used to ensure that the resources can never do something \"bad\". In order to be able to work with individual resources, as well as isolating the complexities that arise from their different interactions, modeling can rely on using global specifications. By keeping specifications as part of the model, there are fewer points of change, which makes for faster and less error-prone development compared to changing the predicates manually, a time-consuming and difficult task.  
SP has no notion of implicit dynamics or memory, i.e., all memory states need to be explicitly modeled using the estimated variables. Often, the decision variables are enough to act as memory, however (they are treated the same as estimated variables). This means that the state of the system is solely defined in terms of the valuations of the variables in the system. In order to constrain the system, it is desired to eliminate all states that violate certain specifications.  
In SP, specifications can be entered as invariant formulas over the system variables that make up the system state. Due to the way automatic transitions (which should always be taken) and effect transitions (which can happen non-deterministically) are defined, these invariant formulas need to be expanded to cover a larger set of states, due to the fact that the system can move uncontrollably between these states.  
To do this, the negation of an invariant formula (i.e., the forbidden states) is extended into larger sets of states using symbolic backwards reachability analysis [22]. After expanding these regions, the symbolic representation is minimized using the espresso heuristic [24] and converted back to a propositional formula that is provided to the planner.  
In the door example, we can specify that it should not be possible for the door to close when the lock is locked. If we use the named predicate \(doorsClosing\) defined earlier, this can be expressed as \(doorsClosing\implies\hat{l}=false\), i.e., whenever the door is closing, the lock is (known to be) unlocked.  
In this case, the result of such a specification will be that the system cannot execute \(gs_{t}:=opened\) when \(\hat{l}\
eq unlocked\) and cannot execute \(l_{t}:=true\) when \(gs_{t}\
eq opened\).  
Similarly, but more simply, a specification can ensure that it should not be possible to open the door when it is locked, mirroring the physical reality. In this case, the use of synthesis is clearly more of a modeling convenience since adding an \"is unlocked\" term to the enabled predicate is easy. However, having it in a specification keeps the interaction between resources in one place. A specification that forbids the door to be closed when \(\hat{l}=\) unknown can be added in the same way. Modeling this uncertainty is conducted so that the system can operate to some degree even in the unknown state, which ensures that a restart after errors can be performed using the control system rather than following a fixed procedure for putting things in a known state.  
Figure 7: Three different plans arising from starting the LockDoor operation in different starting states. In the left-most case, the door is initially opened and the lock is locked. In the middle case, the door is initially opened and the lock is unlocked. To the right, the door is initially closed and the lock is unlocked.