无穷状态系统等价性验证

结题报告
项目介绍
AI项目解读

基本信息

  • 批准号：
    61772336
  • 项目类别：
    面上项目
  • 资助金额：
    63.0万
  • 负责人：
    傅育熙
  • 依托单位：
    上海交通大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2021
  • 批准年份：
    2017
  • 项目状态：
    已结题
  • 起止时间：
    2018-01-01 至2021-12-31

项目摘要

Equality checking on infinite state systems plays a crucial role both in theory and in formal method. The project aims to attack some open problems concerning equality checking on models defined in terms of process rewriting system. The decidability of the branching bisimilarity on epsilon-popping PDA will be investigated, and the completeness issue of the strong bisimilarity on BPA and the complexity of the branching bisimilarity on nBPP will be studied. The principal technical tool we apply is bisimulation tree method we have recently proposed.
无限状态系统的等价性验证既具理论意义，也在形式化方法中有广泛应用。本项目旨在研究有关用进程重写系统定义的若干模型上的等价关系可判定性的若干公开问题。主要考察epsilon-popping PDA的分支互模拟的可判定性、BPA上强互模拟的完备性和nBPP上分支互模拟的复杂性。使用的主要技术是申请人最近提出的互模拟树证明方法。

结项摘要

本研究项目主要取得了四方面进展：.1..开展了交互理论的基础性研究，提出了交互模型假设，证明了现有的一大类模型满足该假定，为进程模型分类和进程度的研究打下了基础。.2..研究了概率模型定义方法，提出了统一的构造概率模型的方法，并提出了研究概率模型语义的统一方法，为概率进程模型研究中的诸多问题提出了一个解决方案。.3..研究了非确定计算的结构，给出了非确定计算谱系的一个公式刻画。.4..证明了带内部动作的无限状态PDA的等价性验证是可判定的，并给出了验证算法。

项目成果

期刊论文数量（9）
专著数量（0）
科研奖励数量（0）
会议论文数量（3）
专利数量（0）
Model independent approach to probabilistic models
概率模型的模型独立方法
  • DOI：
    10.1016/j.tcs.2021.04.001
  • 发表时间：
    2021-04
  • 期刊：
    Model independent approach to probabilistic models
  • 影响因子：
    --
  • 作者：
    Yuxi Fu
  • 通讯作者：
    Yuxi Fu
向量加法系统验证问题研究综述
  • DOI：
    --
  • 发表时间：
    2018
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    张文博;龙环
  • 通讯作者：
    龙环
On the Interactive Power of Higher-order Processes Extended with Parameterization
论参数化扩展的高阶过程的交互能力
  • DOI：
    10.1007/s00165-020-00524-1
  • 发表时间：
    2020-12
  • 期刊：
    Formal Aspects of Computing
  • 影响因子：
    1
  • 作者：
    Wenbo Zhang;Xian Xu;Qiang Yin;Huan Long
  • 通讯作者：
    Huan Long
Counting nondeterministic computations
计算不确定性计算
  • DOI：
    10.1016/j.tcs.2021.08.022
  • 发表时间：
    2021-08
  • 期刊：
    Theor. Comput. Sci
  • 影响因子：
    --
  • 作者：
    Qizhe Yang;Yuxi Fu
  • 通讯作者：
    Yuxi Fu
Modular Verification for Almost-Sure Termination of Probabilistic Programs
概率程序几乎肯定终止的模块化验证
  • DOI：
    10.1145/3360555
  • 发表时间：
    2019-10-01
  • 期刊：
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
  • 影响因子：
    1.8
  • 作者：
    Huang, Mingzhang;Fu, Hongfei;Goharshady, Amir Kafshdar
  • 通讯作者：
    Goharshady, Amir Kafshdar

数据更新时间：{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI：
    {{ item.doi || "--"}}
  • 发表时间：
    {{ item.publish_year || "--" }}
  • 期刊：
    {{ item.journal_name }}
  • 影响因子：
    {{ item.factor || "--"}}
  • 作者：
    {{ item.authors }}
  • 通讯作者：
    {{ item.author }}

数据更新时间：{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ monograph.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ patent.updateTime }}

其他文献

其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI：
    {{ item.doi || "--" }}
  • 发表时间：
    {{ item.publish_year || "--"}}
  • 期刊：
    {{ item.journal_name }}
  • 影响因子：
    {{ item.factor || "--" }}
  • 作者：
    {{ item.authors }}
  • 通讯作者：
    {{ item.author }}
empty
内容获取失败，请点击重试
重试联系客服
title开始分析
查看分析示例
此项目为已结题，我已根据课题信息分析并撰写以下内容，帮您拓宽课题思路：

AI项目思路

AI技术路线图

傅育熙的其他基金

VASS可达性的算法研究
  • 批准号：
    62072299
  • 批准年份：
    2020
  • 资助金额：
    56 万元
  • 项目类别：
    面上项目
进程理论中的否定结果研究
  • 批准号：
    61472239
  • 批准年份：
    2014
  • 资助金额：
    80.0 万元
  • 项目类别：
    面上项目
M-可解性、M-计算复杂性与计算机科学的模型理论
  • 批准号：
    61033002
  • 批准年份：
    2010
  • 资助金额：
    200.0 万元
  • 项目类别：
    重点项目
进程演算的表达能力研究
  • 批准号：
    60873034
  • 批准年份：
    2008
  • 资助金额：
    30.0 万元
  • 项目类别：
    面上项目
灰箱演算的公平性和匿名性研究
  • 批准号：
    60573002
  • 批准年份：
    2005
  • 资助金额：
    25.0 万元
  • 项目类别：
    面上项目
基于进程代数的电子商务协议形式化研究
  • 批准号：
    60473006
  • 批准年份：
    2004
  • 资助金额：
    20.0 万元
  • 项目类别：
    面上项目
内类型理论
  • 批准号：
    69973030
  • 批准年份：
    1999
  • 资助金额：
    10.0 万元
  • 项目类别：
    面上项目
并发计算模型Ｘ－演算的理论研究
  • 批准号：
    69873032
  • 批准年份：
    1998
  • 资助金额：
    11.0 万元
  • 项目类别：
    面上项目
逻辑类型理论的语义及其应用
  • 批准号：
    69503006
  • 批准年份：
    1995
  • 资助金额：
    10.0 万元
  • 项目类别：
    青年科学基金项目

相似国自然基金

{{ item.name }}
  • 批准号：
    {{ item.ratify_no }}
  • 批准年份：
    {{ item.approval_year }}
  • 资助金额：
    {{ item.support_num }}
  • 项目类别：
    {{ item.project_type }}

相似海外基金

{{ item.name }}
{{ item.translate_name }}
  • 批准号：
    {{ item.ratify_no }}
  • 财政年份：
    {{ item.approval_year }}
  • 资助金额：
    {{ item.support_num }}
  • 项目类别：
    {{ item.project_type }}
{{ showInfoDetail.title }}

作者：{{ showInfoDetail.author }}

知道了

AI项目解读示例

课题项目：调控A型流感病毒诱导IFN-β表达的机制研究

AI项目摘要：

本研究聚焦于TRIM2蛋白在A型流感病毒诱导的IFN-β表达中的调控机制。A型流感病毒是全球性健康问题，其感染可导致严重的呼吸道疾病。IFN-β作为关键的抗病毒因子，其表达水平对抗病毒防御至关重要。然而，TRIM2如何调控IFN-β的表达尚未明确。本研究假设TRIM2通过与病毒RNA或宿主因子相互作用，影响IFN-β的产生。我们将采用分子生物学、细胞生物学和免疫学方法，探索TRIM2与A型流感病毒诱导IFN-β表达的关系。预期结果将揭示TRIM2在抗病毒免疫反应中的作用，为开发新的抗病毒策略提供理论基础。该研究对理解宿主抗病毒机制具有重要科学意义，并可能对临床治疗流感病毒感染提供新的视角。

AI项目思路：

科学问题：TRIM2如何调控A型流感病毒诱导的IFN-β表达？
前期研究：已有研究表明TRIM2参与抗病毒反应，但其具体机制尚不明确。
研究创新点：本研究将深入探讨TRIM2在IFN-β表达中的直接作用机制。
技术路线：包括病毒学、分子生物学、细胞培养和免疫检测技术。
关键技术：TRIM2与病毒RNA的相互作用分析，IFN-β启动子活性检测。
实验模型：使用A型流感病毒感染的细胞模型进行研究。

AI技术路线图

        graph TD
          A[研究起始] --> B[文献回顾与假设提出]
          B --> C[实验设计与方法学准备]
          C --> D[A型流感病毒感染模型建立]
          D --> E[TRIM2与病毒RNA相互作用分析]
          E --> F[TRIM2对IFN-β启动子活性的影响]
          F --> G[IFN-β表达水平测定]
          G --> H[TRIM2功能丧失与获得研究]
          H --> I[数据收集与分析]
          I --> J[结果解释与科学验证]
          J --> K[研究结论与未来方向]
          K --> L[研究结束]
关闭
close
客服二维码