在形式化方法研究领域,各种自动机、进程代数系统以及逻辑语言是最常见的用于建模和分析的数学工具。时间自动机、加权自动机和加权时间自动机被用于对带量化信息的系统的建模和分析;进程代数支持并发系统的模块化设计,但它并不能表达基本布尔操作符;空间逻辑、分离逻辑及概率逻辑这类逻辑虽然对于分析并发非确定性系统的性质很有效,但不擅长刻画涉及量化信息的性质。针对这些问题,Kim.G.Larsen提出了并发加权逻辑CWL。CWL是一个多模态的逻辑,其中包含的状态模态词、转换模态词由于带有数字信息,可以有效刻画系统的量化信息。除此之外,CWL特有的组合模态词支持模块化推理和规范,可以用于验证子系统组合形成的上层系统的性质以及系统的全局性质分解产生的模块化性质。但CWL中未涉及不动点算子,而后者对于描述具有无限行为的计算系统的重要性质(如,活性\安全性)具有重要的作用。本文针对CWL开展了进一步研究,主要工作包括如下方面:1.将不动点算子引入CWL,针对其中的一个语言片段(不含系统组合模态词的对偶形式)进行研究,形成并发加权μ-演算μ CWL,针对μ CWL给出了面向μCWL的轮替树自动机。对该自动机的基本性质做了研究,证明了如下两个基本结论:该自动机的非空问题在指数时间内可判定;如果该自动机所接受的语言非空,那么它可以接受一个状态集有限的模型。2.实现了 μCWL与面向μCWL的轮替树自动机互相之间的转换。首先基于公式φ的结构归纳构建了相应的轮替树自动机A(φ),并证明了A(φ)所接受的语言是φ的模型,从而将μCWL的可满足性的可判定性归结为判定面向μ CWL的轮替树自动机的空语言问题。又证明了任意面向μCWL的轮替树自动机A可以转化为μCWL公式φA并且A所接受的语言是φA的模型。3.在上述结果的基础上,研究了 μCWL的基本性质,证明了 μCWL的可满足性的可判定性以及小模型性。基于标记加权转换系统上的互模拟量词,结合面向μCWL的轮替树自动机的性质,证明了 μCWL的一致性内插定理。