为了形式化规范、验证和分析反应式并发系统,学术界提出并发展了多种形式化规范方法。这些方法大体上可分为两类：基于动作的和基于状态的。基于动作的规范方法以进程代数(演算)最具代表性；基于状态的方法通常以模态逻辑或μ-演算描述系统规范。这两类方法基于不同的观点,对形式规范和验证进行了深入而广泛的研究,具有互补的优点：前者支持规范的组合式(compositional)构造、分析和推理；后者擅长描述系统整体和抽象性质。十余年来,学术界期望构建一种允许上述两种不同风格规范并存且混合使用的架构,以此实现可以同时利用它们各自长处的目的。在此愿景驱使下,多种所谓混合规范方法被相继提出,其中,Luttgen和’Vogler近年提出的逻辑标记转换系统(简记为LLTS)克服了其它方法的缺陷,是一个允许自由混合使用通常进程算子和逻辑算子进行规范的语义框架。本文旨在基于纯演算的方法针对LITS在理论研究上的空白和缺陷开展工作,主要工作包括如下方面：(1)构建面向LLTS的进程演算系统CLLR该工作不但将Luttgen和’Vogle r的工作(不含隐藏算子)提升到纯演算的风格,更主要的贡献在于深入研究了他们没有涉及的递归算子。在深入研究环境(context)递归进程的展开与进程转换之间的内在联系基础上,我们较为系统地发展了CLLR的行为理论,证明了Luttgen和’Vogler提出的预备模拟关系相对CLLR所有算子的前同余性(preoongruence)从而在理论上保证了CLLR可以支持规范组合式的构造、分析和推理。作为面向LLTS的演算系统CLLR包含了逻辑合取和析取算子,并需要处理逻辑复合所带来的进程协调性问题。正因为进程协调性对进程行为的发散所具有的敏感性,使得CLLR中的递归算子处理较之通常进程演算要相对困难和复杂许多。(2)在充分考虑协调进程与非协调进程行为差异的基础上,提出了CLLR的公理系统AXCLL,并证明了该系统的可靠性以及相对无递归进程的基完备性,从而揭示了通常进程算子与逻辑合取及析取算子在预备模拟关系下所遵循的代数律。(3)研究了CLLR中形如X=RStx方程的解,证明了唯一解定理和最大解定理。前者给出了这类方程存在唯一解的充分条件；后者揭示了递归进程X X=tx与X=Rs tx的解之间的内在联系：若X是tx的强有卫变元,则X X=tx是满足等式X=RStx的最“粗糙”的规范。(4)作为递归算子与方程最大解定理的应用,我们研究了将基于动作的计算树逻辑ACTL表示安全性质的语言片段在CLLR中进行编码的问题。该研究在理论上保证了CLLR具有描述安全性质的表达能力,同时将判定进程是否满足(表示安全性的)ACTL公式的模型检测问题归约为判定进程之间是否具有精化关系的验证问题。由于递归算子的使用,该工作所提供的编码极大简化了Luttgen和、Voler的原有编码。总之,上述研究将LLTS框架上原有的工作演算化(未包括隐藏算子),在此基础上较深入研究了LUttgen和’Vogler原有工作中没有涉及的若干重要的理论问题,包括：递归算子及其行为理论、方程解以及公理化等,并且本文在ACTL公式编码方面的工作极大简化了他们原有处理方式。与通常进程演算系统比较CLLR的特点在于考虑了进程的逻辑复合以及逻辑复合所带来的协调性问题,允许自由地混合使用通常的进程操作算子、递归算子、逻辑合取和析取算子以及模态词unless和unless(weak until)进行规范描述,并且支持规范组合式构造、推理和分析。