随着计算机技术的飞速发展,复杂系统,例如轨道交通、航空航天、工业控制等的规模和结构越来越庞大和复杂,系统出现缺陷和漏洞的可能性也在不断增加。任何微小错误都足以导致巨大的经济损失,甚至人员伤亡。如何确保复杂系统设计的正确性,是学术界和工业界一直关注的问题。已有研究和实践表明,基于逻辑推理的形式化方法是解决这一问题的有效方法。由于复杂系统普遍具有数据流交换、连续状态、性能指标等特性,传统的逻辑推理方法面临一些新挑战,主要包括如何建立系统行为与性质断言的统一逻辑框架,如何支持组合化、层次化刻画与验证,如何将数学计算过程与逻辑推理过程融合,如何在逻辑框架内建立系统性能的度量标准等。针对这些问题,本文详细研究了刻画系统行为和性质断言的统一逻辑语言,以及逻辑语言的数学模型、证明系统和近似推理系统,并结合实例深入探讨了它们在实际中的应用。本文取得的创新成果归纳如下：(1)提出了具有组合化和层次化特性的多项式代数动态逻辑(ADL),有效地解决了系统行为与性质断言的统一逻辑刻画问题。在ADL的框架中,系统行为被刻画为多项式代数程序,性质断言被刻画为ADL逻辑公式。ADL的组合化特性体现为：多项式代数程序具有组合化的结构,通过顺序、条件、循环等符号将各个子程序组合在一起；层次化则体现为：不同层次之间的关系可被刻画为ADL模态公式,如模态公式[α]φ→[β]φ可表示底层程序a实现了高层程序β的功能。(2)提出了一种更加精细的数学模型——多项式代数变迁系统(ATS),有效地解决了数据流交换、连续状态等的刻画问题。通过引入连续变量,ATS能够描述连续状态,并允许系统具有无限的连续状态空间,因而具有更强的系统刻画能力;通过在系统变迁上标记多项式表达式,ATS能够同时刻画状态跳转和数据流交换,因而可以刻画更加精细的系统行为。更加有意义的是,通过建立系统行为与多项式零点之间的联系,符号计算等成熟的数学方法能够应用于复杂系统的验证分析。(3)建立了ADL的形式化语义和证明系统(ADL演算),有效地解决了数学计算过程与逻辑推理过程的交叉融合问题。以ATS为语义模型,构造了ADL的形式化语义,包括多项式代数程序的变迁语义和逻辑公式的满足关系,变迁语义和满足关系都可用多项式零点定义,因而,逻辑公式的推导问题能够平滑地转化为符号计算的问题。同时,ADL演算是可靠且部分完备的。(4)建立了ADL的度量语义和近似推理系统,有效地解决了系统的性能评估问题。度量语义是对逻辑公式满足关系的一种量化描述,反映了公式成立的可能性,度量语义值越大则公式成立的可能性越高;近似推理系统由一组度量规则构成,用于估算系统性质在给定状态上成立的可能性。同时,近似推理系统是可靠的,而且是对ADL演算的量化扩展：凡是ADL演算可证的公式必定是可近似推导的。最后,本文对两个实例进行了验证与分析。实例分析结果表明,本文所建立的方法能够有效地刻画、验证和分析复杂系统的性质。