Refactoring [7][8]是自動化地透過一些等價的轉換(equivalence transformations) 來打破系統舊有的模組性 (as-built modularity) 以創造出新的系統架構。使得局部性分析在新的系統架構底下能夠發揮 divide and conquer 的優點以避免組態爆炸。在使用Refactoring轉移系統時，必需確保所架構之新系統與原系統是等價的。此等價關係曾借用弱等價(weak bisimulation) 來描述，但是弱等價並不能保留重要的性質如 liveness。在本論文中，我們使用程序代數的方式建立公設化代數結構，證明使用Refactoring所轉成的新系統與原系統是具有congruence的等價關係。
建立公設化代數結構，並將代數結構中每一元素適當的對應到實際系統的每一個活動，此代數結構即可正確的模擬系統行為，驗證系統的性質。以代數結構模擬系統有許多好處，諸如整個數學邏輯供我們使用、用數學語言表示系統行為等。對不同的系統行為，有不同的公設，形成不同的公設化代數結構，因此在所研究的領域裡，首先找出一核心公設化代數結構，適用於領域中任意系統，再跟據不同的應用增加公設，就像數學中群、環、體的延伸。

Design model refactoring [7][8] is applying a set of equivalence transformations automatically to change the as-built modularity of a design model. The refactored model (with new structure) is more amenable to compositional analysis for avoiding state explosion because it’s structure could maximizes the power of divide and conquer method. To preserve properties of interests, each refactoring transformation is designed to maintain the behavioral equivalence. In [7][8], we adopt weak bisimulation as our equivalence. However, weak bisimulation is too weak to preserve useful properties such as liveness. In this thesis, we use process algebra to construct an axiomized algebra. It can be used to prove that the systems before and after refactoring have congruence equivalence relation.
We first construct an axiomized-algebra and map each element in the algebra structure to an action in real systems (such as an synchronization between concurrent processes). Therefore, the algebra can be used to model behaviors of systems and verify system properties. There are some advantages for modeling systems by algebra: We can use mathematical languages and logics to express and reason system behaviors. For different definitions of system behaviors, we can use different set of axioms to define different algebra. In this thesis, we first define a core set of axioms which is applicable to any systems. Next, depending on the needs of applications, we add more axioms to the system, like extending from group, rings, to field in mathematics.