在局部性分析中，窮舉所有子系統的狀態時，常常會出現有多餘的狀態產
3.2.1. 環境介面行程(Environment Interface Process)
在 Cheung 和 Kramer[29]的研究中提到，在子系統列舉狀態時，加入環境介 面行程（Environment Interface Process, EIP）一併合成，多餘的狀態將可被減化。
而環境介面行程可以經由下列三個步驟產生：
（1）簡化環境行程（environment process）：在整個系統中，不包括在此子 系統內的行程，皆為此子系統的環境行程。但不是每一個環境行程都會和此子系 統有本文限制的關係。我們會將所有的行程與 export set 中的 actions 逐一比對，
如果該環境行程有和 export set 擁有相同且兩個以上的 actions，才是和該子系統 有本文限制關係的環境行程。
接 著 我 們 會 從 這 些 篩 選 出 來 的 環 境 行 程 中 ， 刪 除 與 該 子 系 統 無 關 的 transitions，也就是與 export set 無關的 actions，都會被移除。
（2）將所有環境行程轉換為可決定性（deterministic）：簡化後的環境行程，
必須是可決定性的，如果為不可決定性的（non- determine）則必須轉換為可決定 性的 LTS。不可決定性的 LTS 是指在同一個狀態中，兩個不同的 transition，卻 有著相同 label 的 actions。可決定性的 LTS 中，每個狀態中的 action 不會重覆。
（3）合成所有環境行程：經由步驟(2)所得到可決定性的環境行程，若有兩 個以上，則需合成為一個。最後合成的結果即為環境介面行程。在 ArCats 中，
此功能已被實作為 genInterface [33]，在子系統合成之前，先經由 genInterface 得 到 EIP。然後再將 EIP 加入子系統一併進行狀態的合成，展開後所產生的新行程，
會移除掉無法到達的狀態，減緩組態爆炸的發生。
3.2.2. 本文限制的合成規則
Figure 3-1 Compose processes P and Q, and EIP
平行合成的初始狀態為(000)，(000)狀態中的第一個 transition 上的 label 為 -c，我們將-c 這個 label 和狀態(000)逐一做 Com1、Com2 和 Com3 三種合成規則
的檢查。由於-c 不存在於 export set 中，故不符 合 Com1。接著 進行 Com2 的檢查，
(000)狀態中的下一個 transition 的 label 為 c，-c 和 c 是一配對行為，經由 Com2
後將此配對行為隱藏為τ，所以(P || Q)的平行合成結果會由原本的狀態(000)，經 由行為τ，而到達新狀態(110)。我們將此新狀態(110)展開後，並將其存入 vector 中，等待之後繼續展開此新狀態。此時(P || Q)的結果如 Figure 3-2 表示。
Figure 3-2 Composition of (P || Q) by Com2
(000)狀態的第二個 transition 的 label 為 c，而 c 存在於 export set 中，故符合
Com1。由於此例中加入了本文限制的合成規則 Com3，所以我們繼續做 Com3 的檢查，確認此處的 c 是否會受到本文限制而無法展開。
此時合成引擎會到 EIP 中檢查是否有可以產生配對行為的 label，EIP 目前的 狀態為 0，狀態 0 有一 transition 的 label 為 -c，且可以藉由-c 由狀態 0 轉移至狀 態 1，表示 c 這個 action 沒有受到本文限制，所以經由 Com3 的合成規則，(P || Q)
的平行合成結果會由狀態(000)會產生一個 label 為 c 的 transition 而到達新狀態 (010)，如 Figure 3-3 所示。
Figure 3-3 Composition of (P || Q) by Com1 and Com3
此時(000)狀態中的所有 transitions 都已檢查完畢，所以我們從 vector 中提出 新狀態(110)繼續拓展，步驟皆如同上述方式，對每個狀態中的每個 transition 逐 一檢查上述三種合成規則，若可以符合其中一項規則且沒有受到本文限則，即可 得到新的 action 和新狀態。最後的合成狀態以 Figure 3-4 表示。
Figure 3-4 Composition of (P || Q) with Context Constraint
如果(P || Q)沒有使用本文限制的合成規則，則平行合成的結果如 Figure
3-5，會產生多餘的移轉 c 以及-a，以及多餘的狀態(10)，以灰階表示。由於這類 不可到達的狀態，對後續的子系統合成並無任何幫助，所以應使用本文限制的 合成規則儘早將其移除。
Figure 3-5 Composition of (P || Q) without Context Constraint