在形式化方法研究领域,转换系统是描述软件或硬件系统行为的一种重要形式化模型。近年来,针对实时系统、控制系统及最优化问题等实际系统的建模需要,学术界提出了诸多带有量化信息的转换系统。对于这些系统而言,传统的互模拟概念不适合描述系统间的行为等价性。为了克服这一缺陷,研究者们提出了众多近似等价概念并开展了较深入的理论和应用研究。本文将就带有量化信息的转换系统的近似等价理论开展研究,全文工作分为理论研究与应用研究两部分。理论研究方面的主要工作包括如下方面：(1)近似互模拟与距离函数是定义系统近似等价的两种主要方法,在度量化的转换系统的框架下,应明生教授和Breugel采用这两种方法分别提出了λ-互模拟和行为拟度量。本文研究了两者之间的关系,否定了Breugel的猜想,建立了λ-互模拟诱导出的λ-行为拟度量的不动点特征。(2)在量化转换系统框架下,本文将折扣的思想引入近似互模拟的定义中,提出了(η,α)-互模拟概念,其中参量η表示状态之间的近似程度,α是一个折扣因子。本文给出了(η,α)-互模拟的一些基本性质,研究了(η,α)-互模拟与Girard和Pappas提出的δ-近似互模拟之间的关系,建立了(η,α)-互模拟的分层刻画,并探讨了(η,α)-互模拟诱导出的距离函数的相关性质。在量化转换系统框架下,de Alfaro等人提出了分岔距离用于描述系统的行为近似等价性。本文讨论了(η,α)-互模拟与分岔距离之间的关系,利用(η,α)-互模拟给出任意折扣下分岔距离的互模拟刻画,从而将Girard和Pappas关于无折扣分岔距离的互模拟刻画的结果推广到一般情形。本文还证明了,在非死锁和有限分岔的量化转换系统中,(η,α)-互模拟也可以由分岔距离刻画。这些结论揭示了(η,α)-互模拟与分岔距离之间的内在联系。(3)交替转换系统是一种刻画开放式系统的重要形式化模型。针对一类特殊的交替转换系统,Po1a和Tabuada定义了交替近似互模拟的概念用于刻画带扰动控制系统与其有限抽象之间的关系。本文将这个概念推广到一般的交替转换系统中,探讨了交替近似互模拟的基本性质,并提出了一种近似互模拟模态特征表述方式,基于交替时序逻辑给出了交替近似互模拟的逻辑特征,从而建立了交替转换系统间行为近似等价性与其所满足的逻辑性质之间的内在联系。应用研究方面的工作侧重解决带扰动线性控制系统的形式化设计中遇到的若干问题。控制系统的形式化设计旨在利用形式化的方法构造控制系统的反馈控制器使得控制系统在该控制器作用下满足给定的规范。最近几年,学术界已经就无扰动控制系统的形式化设计展开了一系列研究。在这些工作中,为了降低控制系统的状态空间的规模,研究者们通常构造控制系统的有限抽象系统,进而通过构造有限抽象系统的控制器得到原控制系统的控制器。本文试图将这一技术路线推广到带扰动线性控制系统的形式化设计中,主要工作包括：(4)本文给出了一个控制策略算法用于构造带扰动线性控制系统的有限抽象的控制策略。在无扰动情形下,控制系统的有限抽象一般是经典的转换系统。文献中给出了诸多算法用于求解无扰动情形下控制系统的有限抽象的控制策略。然而,在带扰动输入的情形下,经典的转换系统无法刻画可控输入和扰动输入之间的差别。为了克服这一缺陷,Pola和Tabuada采用交替转换系统作为带扰动控制系统与其有限抽象的形式化模型,这导致在无扰动情形下提出的各种算法不适用于求解带扰动控制系统的有限抽象的控制策略。本文基于Kabanza等人提出的规划算法给出了一个控制策略算法用于求解控制策略。具体而言,对给定的有限交替转换系统和线性时序逻辑公式,该算法可以用于寻找初始状态和控制策略使得交替转换系统可控满足给定的线性时序逻辑公式。(5)本文证明了上述控制策略算法的正确性,并就一类时序逻辑公式证明了它的完备性。我们基于完全的Buchi自动机定义了完全公式概念,并证明对于完全公式而言,上述控制策略算法是完备的,即,给定有限交替转换系统和完全的线性时序逻辑公式,如果存在初始状态和控制策略使得交替转换系统在该控制策略作用下从该初始状态出发的所有轨迹均满足给定的线性时序逻辑公式,则上述控制策略算法必然可以找到所需的初始状态和控制策略。(6)本文提出了一种基于有限抽象构造带扰动控制系统控制器的方法。在无扰动情形下,学术界先后分别基于互模拟和近似互模拟提出了两种方法用于控制系统的形式化设计。这两种方法采用了相近的技术路线,即,构造与原系统互模拟(或近似互模拟)的有限抽象,进而通过构造有限抽象的控制器得到原控制系统的控制器。基于与原系统互模拟的有限抽象构造的控制器可以确保控制系统在其作用下严格满足给定规范。然而,由于互模拟要求严格,与原系统互模拟的有限抽象较难构造。Girard和Pappas退而求其次,提出了基于与原系统近似互模拟的有限抽象的控制器设计方法。这样的有限抽象相对容易构造,但该方法构造的控制器仅能确保控制系统近似满足给定规范。我们基于本文交替近似互模拟逻辑特征的工作,针对带扰动控制系统提出了另一种控制器形式化设计思路。本文方法的核心在于规范的转换。我们提出了两个规范转换函数,基于转换后的规范构建有限抽象系统的控制器,由此保证原系统严格可控满足原规范。该方法兼顾上述两种方法的优点,既保持了有限抽象的易构性,同时还可以确保系统在构造出的控制器作用下严格满足给定规范。需要指出的是,与其他两种方法相比,本文方法的缺陷在于可能降低有限抽象的控制器存在的可能性。