## Appendix A
\begin{array}{ll}1^{\prime}(R,60)&if\ p=EW\_GS\_R_{sock}^{in/out }(phase3)\\ 1^{\prime}(Y,0)&if\ p=EW\_TL\_T_{sock}^{in}(phase3)\\ 1^{\prime}(R,0)&if\ p=NS\_GS\_R_{sock}^{in}(phase3)\\ 1^{\prime}(R,30)&if\ p=NS\_TL\_R_{sock}^{in/out}(phase3)\\ 1^{\prime\prime}\textit{PR\_RT}^{\prime\prime}&if\ p=Transit\ Priority\ Request(red\ truncation)\\ \varnothing&\textit{otherwise}\end{array} \right.\]  
in \(M_{9}\), transition phase3 is enabled, it can fire. Firing the enabled transition phase3 at marking \(M_{9}\) yields marking \(M_{10}\), it means that the go-straight green lights in north-southward traffic direction turn on and continue for 27 s.  
\[M_{10}(p)=\left\{ \begin{array}{ll}1^{\prime}(R,60)&if\ p=EW\_GS\_R_{sock}^{ in/out}(phase3)\\ 1^{\prime}(R,60)&if\ p=EW\_TL\_R_{sock}^{out}(phase3)\\ 1^{\prime}(G,27)&if\ p=NS\_GS\_G\_(phase3)\\ 1^{\prime}(R,30)&if\ p=NS\_TL\_R_{sock}^{in/out}(phase3)\\ 1^{\prime\prime}\textit{PR\_RT}^{\prime\prime}&if\ p=Transit\ Priority\ Request(red\ truncation)\\ \varnothing&\textit{otherwise}\end{array} \right.\]  
in marking \(M_{10}\), the transition firing sequence \({(c4)}^{27}t41{(c41)}^{3}\) can be executed and results in a new marking \(M_{11}\), which enables the transition phase4 in Figure 4e. \[M_{11}(p)=\left\{ \begin{array}{ll}1^{\prime}(R,30)&if\ p=EW\_GS\_R_{sock}^{ in}(phase4)\\ 1^{\prime}(R,30)&if\ p=EW\_TL\_R_{sock}^{in}(phase4)\\ 1^{\prime}(Y,0)&if\ p=NS\_GS\_Y_{sock}^{in}(phase4)\\ 1^{\prime}(R,0)&if\ p=NS\_TL\_R_{sock}^{in}(phase4)\\ 1^{\prime\prime}\textit{PR\_RT}^{\prime\prime}&if\ p=Transit\ Priority\ Request(red\ truncation)\\ \varnothing&\textit{otherwise}\end{array} \right.\]  
After phase4 fires, a new state which means that the turn-left green light in north-southward traffic direction is generated and is represented as the following marking:  
\[M_{12}(p)=\left\{ \begin{array}{ll}1^{\prime}(R,30)&if\ p=EW\_GS\_R_{sock}^{ in}(phase4)\\ 1^{\prime}(R,30)&if\ p=EW\_TL\_R_{sock}^{in}(phase4)\\ 1^{\prime}(R,30)&if\ p=NS\_GS\_R_{sock}^{out}(phase4)\\ 1^{\prime}(G,27)&if\ p=NS\_TL\_G_{sock}^{out}(phase4)\\ 1^{\prime\prime}\textit{PR\_RT}^{\prime\prime}&if\ p=Transit\ Priority\ Request(red\ truncation)\\ \varnothing&\textit{otherwise}\end{array} \right.\]  
In Figure 3, besides the green extension priority strategy, the red truncation priority strategy is also illustrated. A specific system state \(M_{13}\) which can be generated by the execution of transition firing sequence \({(c5)}^{17}\) is considered to illustrate this strategy. \[M_{13}(p)=\left\{ \begin{array}{ll}1^{\prime}(R,13)&if\ p=EW\_GS\_R_{sock}^{ in}(phase4)\\ 1^{\prime}(R,13)&if\ p=EW\_TL\_R_{sock}^{in}(phase4)\\ 1^{\prime}(R,13)&if\ p=NS\_GS\_R_{sock}^{out}(phase4)\\ 1^{\prime}(G,10)&if\ p=NS\_TL\_G_{sock}^{out}(phase4)\\ 1^{\prime\prime}\textit{PR\_RT}^{\prime\prime}&if\ p=Transit\ Priority\ Request(red\ truncation)\\ \varnothing&\textit{otherwise}\end{array} \right.\]\(M_{13}\) indicates that transition c5 is enabled and fires 17 times continuously until the residual red time in EW_GS_R is reduced to 13 s. Suppose that at this time, an approaching transit vehicle is detected in east-westward traffic direction, then the transition Init2 in Figure 4e is enabled. After it fires, a new marking is generated by making the occurrence of \(M_{13}[Init2>M_{14}\), then transition red truncation in Figure 4e is enabled, which means the residual red time in east-westward traffic direction can be truncated. \(M_{14}(p)=\left\{ \begin{array}{ll}1^{\prime}(R,13)&if\ p=EW\_GS\_R^{in/out}_{ sock}(red\ truncation)\\ 1^{\prime}(R,13)&if\ p=EW\_TL\_R^{in/out}_{sock}(red\ truncation)\\ 1^{\prime}(R,13)&if\ p=NS\_GS\_R^{in/out}_{sock}(red\ truncation)\\ 1^{\prime}(G,10)&if\ p=NS\_TL\_G^{In/out}_{sock}(red\ truncation)\\ 1^{\prime}10&if\ p=EW\_GS\_RT\\ \varnothing&\text{otherwise}\end{array} \right.\)  
After transition red truncation fires, a new state is obtained by making the occurrence of \(M_{14}[\text{\emph{red truncation}}>M_{15}\):  
\(M_{15}(p)=\left\{