一般硬件系统和软件系统都存在大量的相同的或同构的组件,相应地,它们的模型常常在结构上存在对称性,这种对称结构一般具有相同或非常相近的性质。人们为了使问题简化,根据这种情况开发了对称约简算法来简化模型。特别是在形式化验证中,对称约简方法已经成为解决状态爆炸问题的有效方法之一。进程代数已经是刻画并发系统的最普遍、最常用的描述语言,而事件结构也是刻画真并发系统的强有力的建模工具,它们常常展示出对称性。然而,当前大多数研究都集中在基于变迁系统模型的对称约简,从未涉及这两种建模工具的对称性方面的研究。在本文中,我们对进程代数语言和事件结构模型的对称约简进行了深入研究。这些工作力图从结构上建立对建模语言和模型进行约简的基本理论,目的是希望从结构上建立起类似于行为等价的由细到粗的约简体系,为开发复杂系统而建立的不同层次静态约简模型服务。另一方面,自顶向下逐步细化的层次化设计方法是人们广泛接受的设计计算机硬件系统和软件系统的最主要方法之一。动作细化是系统层次化刻画方法的核心操作,这一理论的研究一般在进程代数和事件结构模型中进行的,已经取得了丰硕的成果。在此基础上,我们研究了对称约简对动作细化的影响,同时研究了交织等价和步进等价在动作细化下的保持问题。本文针对进程代数语言提出了进程的对称性概念,给出了对称约简算法,并证明了约简后的进程与原进程是交织迹和交织互模拟等价的,同时提供了两个有意义的实例来说明对称性的定义并验证了约简算法的正确性。接下来,针对事件结构模型我们提出了基于置换群的对称性概念。在事件结构中,引入了事件结构的商结构模型,证明了商结构与原事件结构是迹、互模拟和偏序多集迹等价的,建立了针对事件结构的对称约简算法,得出了对称约简不影响等价在动作细化下的保持。在研究了事件结构的对称性之后,进一步从理论上比较对称约简与自互模拟约简的区别和联系。交织等价(即交织迹等价和交织互模拟等价)与步进等价(即步进迹等价和步进互模拟等价)在动作细化下是不保持的。一些工作研究了交织互模拟等价在严格限制动作细化的情况下才能保持,但在这种限制下交织迹等价仍然不保持,没有工作进一步讨