量化进程的语义

The success of the classical process algebras in formal specification and verification has led to the change of our investigation of concurrent systems from qualitative to quantitative analysis. Two typical kinds of processes with quantitative information, called quantitative processes, are probabilistic and quantum processes. This project focuses on the operational and denotational semantics of quantitative processes. More specifically, we study the behavioural equivalences and similarities of quantitative processes from four different perspectives: multi-success testing, behavioural pseudometric, bisimulation and linear contextual equivalence. This will enhance the semantic foundations of quantitative processes, and thus provide theoretical support for future analysis and verification of quantitative concurrent systems. In addition, we will distill.some useful techniques and methods of studying quantitative processes, and generalize some important ideas from probabilistic process algebra to quantum process algebra.

经典进程代数在形式化规范和验证中的成功应用和发展促使人们对并发系统的认识逐渐由定性分析转变到定量分析。两类有代表性的带有量化信息的进程（量化进程）是概率进程和量子进程。本项目研究量化进程的操作语义和指称语义。具体而言，我们将从多目标测试、行为度量、互模拟和线性上下文等价这四个方面深刻认识进程的行为等价和相似度，加强量化进程的语义基础，为今后分析和验证量化并发系统提供理论支持。此外，通过本项目，我们将提炼研究量化进程的语义时一些常用的技巧与方法，从而把有关重要思想从概率进程代数推广到量子进程代数。

经典进程代数在形式化规范和验证中的成功应用和发展促使人们对并发系统的认识逐渐由定性分析转变到定量分析。两类有代表性的带有量化信息的进程(量化进程)是概率进程和量子进程。经过四年的努力，我们对量化进程的形式化语义有更深入的了解,已经取得阶段性的成果，具体反映在如下几个方面：（1）为概率进程和模糊进程提出基于状态和基于分布两种互模拟度量，并给出模态逻辑刻画，其中对基于状态概率互模拟的刻画极大简化了文献中已有方法;（2）提出概率程序的敏感性和代价分析方法以及时滞概率程序在给定时间界下终止概率分析方法；（3）把概率互模拟的思想拓展到量子进程代数，实现量子基互模拟判定算法，并开发工具检验量子超密编码、量子隐形传态、量子秘密共享、量子密钥分发等协议的功能正确性；（4）设计并实现了一款轻量级的量子模拟器工具Qsimulation，已推出2.0版本，其性能优于Qiskit和ProjectQ两个开源工具。以上结果为我们将来深入研究量子程序验证打下了坚实的基础。