进程理论中的否定结果研究

批准号:
61472239
项目类别:
面上项目
资助金额:
80.0 万元
负责人:
傅育熙
依托单位:
学科分类:
F0201.计算机科学的基础理论
结题年份:
2018
批准年份:
2014
项目状态:
已结题
项目参与者:
尹强、张文博、陶秀挺、肖可君、田生、谢晓青、柳萌宇、白吉光、徐珂
国基评审专家1V1指导 中标率高出同行96.8%
结合最新热点,提供专业选题建议
深度指导申报书撰写,确保创新可行
指导项目中标800+,快速提高中标率
微信扫码咨询
中文摘要
否定结果在数学、数理逻辑、计算机科学中扮演着重要角色。在进程理论中,否定结果能推进进程理论向深度发展。本申请项目拟探索进程理论中有重要意义的否定结果,主要考察两个方面:一、研究进程表达能力的否定结果,即证明一个模型的表达能力不比另一个强,或两个模型的表达能力不一致等结果。表达能力的否定结果是建立现有模型之间关系图的关键步骤。二、研究不可有限公理化问题,主要研究有限状态进程上等价关系的不可有限公理化问题,这里有限公理化是指不使用规不动点归纳的完备系统。不可有限公理化方面的结论不仅对设计验证系统有实际应用,而且对模型设计和算子选择具有指导意义。本申请项目的意义在于通过探索具有重要意义的否定结果,推进进程理论证明技术和低层理论的研究,加快进程理论的深度研究以及对模型无关的核心理论的探讨。
英文摘要
Negative results play a crucial role in mathematics, logic and computer science. In process theory, negative results help reveal the depth of the theory. The project aims to investigate some negative results in process theory. Two aspects will be studied. Firstly we attempt to prove some negative results on expressiveness. By showing that one model is not as expressive as another, or that two models are incompatible with each other in terms of expressiveness, we advance our understanding of process theory in particular and concurrency theory in general. Secondly we look at the non-axiomatisability issue of the finite states, focusing mainly on equational systems without using the fixpoint induction. Results obtained in this direction are useful to the construction of verification systems. It is expected that the techniques developed in this have wide applications in process theory.
本项研究取得四项进展。一、否定了此前有关高阶进程演算和一阶pi-演算之间关系的伪命题。我们证明了:一般地,高阶演算无法在一阶pi-演算中得到解释,故高阶进程模型的表达能力不超过一阶pi-演算的结论是错误的。我们还研究了高阶模型的若干变种之间的表达能力关系。二、我们提出了extensional Petri网模型,在该模型中,Petri网是可复合的,这解决了传统Petri网不可复合的问题。三、我们加强了Senizergues获得哥德尔奖的结果,证明了epsilon-pushing nPDA和epsilon-popping PDA均为可判定的。这方面的两篇文章尚在审稿中。最后,我们研究了C-图的计数问题,证明了不确定计算的结构是非常复杂的。这方面的一篇文章也在审稿中。
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
DOI:10.1080/00207160.2016.1210793
发表时间:2017-07
期刊:INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS
影响因子:1.8
作者:Yin Qiang;Xu Xian;Long Huan
通讯作者:Long Huan
DOI:10.23638/lmcs-13(4:11)2017
发表时间:2017-08
期刊:Logical Methods in Computer Science
影响因子:0.6
作者:Fu Yuxi
通讯作者:Fu Yuxi
DOI:--
发表时间:2018
期刊:软件学报
影响因子:--
作者:张文博;龙环
通讯作者:龙环
Analyzing data flow diagrams by combination of formal methods and visualization techniques
结合形式化方法和可视化技术分析数据流图
DOI:10.1016/j.jvlc.2018.08.001
发表时间:2018-10
期刊:Journal of Visual Languages and Computing
影响因子:--
作者:Zhang Haocheng;Liu Wei;Xiong Hao;Dong Xiaoju
通讯作者:Dong Xiaoju
VASS可达性的算法研究
- 批准号:62072299
- 项目类别:面上项目
- 资助金额:56万元
- 批准年份:2020
- 负责人:傅育熙
- 依托单位:
无穷状态系统等价性验证
- 批准号:61772336
- 项目类别:面上项目
- 资助金额:63.0万元
- 批准年份:2017
- 负责人:傅育熙
- 依托单位:
M-可解性、M-计算复杂性与计算机科学的模型理论
- 批准号:61033002
- 项目类别:重点项目
- 资助金额:200.0万元
- 批准年份:2010
- 负责人:傅育熙
- 依托单位:
进程演算的表达能力研究
- 批准号:60873034
- 项目类别:面上项目
- 资助金额:30.0万元
- 批准年份:2008
- 负责人:傅育熙
- 依托单位:
灰箱演算的公平性和匿名性研究
- 批准号:60573002
- 项目类别:面上项目
- 资助金额:25.0万元
- 批准年份:2005
- 负责人:傅育熙
- 依托单位:
基于进程代数的电子商务协议形式化研究
- 批准号:60473006
- 项目类别:面上项目
- 资助金额:20.0万元
- 批准年份:2004
- 负责人:傅育熙
- 依托单位:
并发计算模型X-演算的理论研究
- 批准号:69873032
- 项目类别:面上项目
- 资助金额:11.0万元
- 批准年份:1998
- 负责人:傅育熙
- 依托单位:
逻辑类型理论的语义及其应用
- 批准号:69503006
- 项目类别:青年科学基金项目
- 资助金额:10.0万元
- 批准年份:1995
- 负责人:傅育熙
- 依托单位:
国内基金
海外基金
