# 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  
Note that the model \(G\) of a CPPS is an abstraction of the underlying production system. The minimal resource requirements must be satisfied for the CPPS to run and manufacture the products of an order. The minimal resource requirements for the model \(G\) of a CPPS can be represented by a marking \(m^{*}\), where \(m^{*}(p)=\left\{ \begin{array}{l}\sum\limits_{j\in I}\sum\limits_{i\in T}R_ {jt}(r)\forall p\in P_{o}\\ 0\ p\in P\backslash P_{o}\end{array} \right..\)  
The Future States Awareness Problem is concerned with whether the target marking \(m_{f}\) can be reached without visiting any undesirable states. In Petri net theory, the concept of liveness property ensures that undesirable states will not be visited. Therefore, we solve the Future States Awareness Problem based on the concept of liveness in Petri nets. We define the liveness of \(G_{c}(m_{0},u)\) as follows. Definition 12: \(G_{c}(m_{0},u)\) is live if for each marking reached from \(m_{0}\) under \(u\), each transition can still be fired ultimately by progressing through some further firing sequence. For the existence of a control policy \(u\) under which \(G_{c}(m_{0},u)\) is live, there must be sufficient resources under the initial marking \(m_{0}\). In this paper, it is assumed that the initial marking \(m_{0}\) satisfies the condition: \(m_{0}\geq m^{*}\). Under this assumption, the following property states a liveness condition for the model \(G\) of a CPPS. Property 1: \(G_{c}(m_{0},u)\) is live under a control policy \(u\) if and only if there is a sequence of control actions that can bring each marking \(m\) reached under control policy \(u\) to \(m^{\prime}\) with \(m^{\prime}\geq m^{*}\). Proof:  
Sufficiency:  
We must prove that if there is a sequence of control actions \(c_{1}c_{2}c_{3}...c_{n}\) that can bring each marking \(m\) reached under control policy \(u\) to \(m^{\prime}\) with \(m^{\prime}\geq m^{*}\), \(G_{c}(m_{0},u)\) is live under the control policy \(u\). To show that \(G_{c}(m_{0},u)\) is live under the control policy \(u\), we must show that each transition can still be fired by progressing through some further firing sequence from \(m^{\prime}\). Note that \(m^{\prime}\geq m^{*}\). The resources under \(m^{\prime}\) satisfy the minimal resource requirements. Therefore, we can construct a sequence of control actions to fire transition \(t_{jn}\) in type-\(j\) task subnet by firing \(t_{j0},t_{j1},t_{j2},...,t_{j(n-1)},t_{jn},...,t_{jN_{j}},t_{j(N_{j}+1)}\) sequentially. As the requirements to fire transition \(t\) in \(T_{j}\) is \(R_{jt}(r)\leq m^{*}(r)\forall r\in R\), the firing sequence \(t_{j0},t_{j1},t_{j2},...,t_{j(n-1)},t_{jn},...,t_{jN_{j}},t_{j(N_{j}+1)}\) can be fired. Therefore, transition \(t_{jn}\) can be fired by progressing through the firing sequence \(t_{j0},t_{j1},t_{j2},...,t_{j(n-1)},t_{jn}\). Let \(m^{\prime\prime}\) be the marking reached after firing \(t_{j0},t_{j1},t_{j2},...,t_{j(n-1)},t_{jn},...,t_{jN_{j}},t_{j(N_{j}+1)}\). Under \(m^{\prime\prime}\), all the resources return to the idle state. Hence \(m^{\prime\prime}\geq m^{*}\) and every transition can be fired again by progressing through some firing sequence again. Based on the above reasoning, each transition can still be fired by progressing through some further firing sequence from \(m^{\prime}\). Therefore, \(G_{c}(m_{0},u)\) is live under the control policy \(u\). Necessity:  
Let \(m\) be a marking reached under the given control policy \(u\). We prove by constructing a firing sequence that can bring \(m\) to \(m^{\prime}\) with \(m^{\prime}\geq m^{*}\). We first construct a firing sequence that can bring \(m\) to \(m^{\prime}\) under which all the resources are returned to an idle state. As \(G_{c}(m_{0},u)\) is live under a control policy \(u\), for each marking reached from \(m_{0}\) under \(u\), each transition can still be fired by progressing through some further firing sequence.