# A Theoretical Foundation for Context-Aware Cyber-Physical Production Systems
## 5 Approach to Deadline Awareness Problem and Future States Awareness Problem
### Analysis of the CPPS Model
There must exist a firing sequence \(s\) from \(m\) such that the last transition \(t_{j(N_{j}+1)}\) is fired at least \(\sum\limits_{n=0}^{N_{i}}m(p_{jn})\) times for each type-\(j\) task subnet, \(j\in J\). We construct a firing sequence \(s^{\prime}\) based on \(s\) to complete all the remaining tasks under \(m\) without introducing new tasks as follows. Consider a type-\(j\) task subnet, where \(j\in J\). As transition \(t_{j(N_{j}+1)}\) of type-\(j\) task subnet is fired at least \(\sum\limits_{n=0}^{N_{j}}m(p_{jn})\) times, firing sequence \(s\) from \(m\) can be represented as \(s=s_{1}s_{2}\), where transition \(t_{j(N_{j}+1)}\) appear in \(s_{1}\) exactly \(\sum\limits_{n=0}^{N_{j}}m(p_{jn})\) times. Note that firing sequence \(s_{1}\) may contain transition \(t_{j0}\) and transition \(t_{j0}\) may appears a number of times in \(s_{1}\). This means that transition \(t_{j0}\) may also be fired in \(s_{1}\) a number of times. Firing transition \(t_{j0}\) will bring new task (s) into type-\(j\) task subnet and may make the transitions at the downstream fired in \(s_{1}\). We construct a firing sequence \(s^{\prime}_{1}\) based on \(s_{1}\) by removing transition \(t_{j0}\) and all relevant transitions at the downstream of \(t_{j0}\) fired in \(s_{1}\). Removing the transitions of new tasks from \(s_{1}\) reduces the number of resources to be used for firing transitions. As \(s_{1}\) can be fired from \(m\), the resulting firing sequence \(s^{\prime}_{1}\) can also be fired from \(m\). Note that all the remaining operations in the existing tasks in type-\(j\) task subnet under \(m\) will be completed after firing \(s^{\prime}_{1}\). Therefore, all the resources required by type-\(j\) task subnet will return to the idle state. In this way, we have constructed a firing sequence \(s^{\prime}_{1}\) that can be fired from \(m\). Note that the firing sequence \(s^{\prime}=s^{\prime}_{1}s_{2}\) is still a valid firing sequence that can be fired from \(m\) and transition \(t_{j^{\prime}(N_{j^{\prime}+1})}\) of type-\(j^{\prime}\) task subnet is fired at least \(\sum\limits_{n=0}^{N_{j}}m(p_{jn})\) times in \(s^{\prime}=s^{\prime}_{1}s_{2}\) for each type-\(j^{\prime}\) task subnet, where \(j^{\prime}\in J\backslash\{j\}\). Therefore, we can follow a similar procedure to construct a firing sequence \(s^{\prime\prime}\) to complete all the remaining operations in the existing tasks in each type-\(j^{\prime}\) task subnet under \(m\) for each \(j^{\prime}\in J\backslash\{j\}\) one by one. After firing \(s^{\prime\prime}\) from \(m\), a marking \(m^{\prime}\) will be reached and all the resources required by each type of task subnets will return to the idle state under \(m^{\prime}\). Due to the conservation of resources, the set of resources in an idle state under \(m^{\prime}\) is the same as that under \(m_{0}\), therefore, \(m^{\prime}\geq m_{0}\). As \(m_{0}\geq m^{*}\), \(m^{\prime}\geq m^{*}\). Therefore, we have proved that the firing sequence \(s^{\prime\prime}\) that can bring \(m\) to \(m^{\prime}\) with \(m^{\prime}\geq m^{*}\). Let \(c_{1}\), \(c_{2}\),..., \(c_{\tau}\) be the sequence of control actions associated with the firing sequence \(s^{\prime\prime}\). Hence, there is a sequence of control actions \(c_{1}\), \(c_{2}\),..., \(c_{\tau}\) that can bring each marking \(m\) reached under control policy \(u\) to \(m^{\prime}\) with \(m^{\prime}\geq m^{*}\). This completes the proof. \(\square\)