线形时态逻辑的可满足性理论与应用研究

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

基本信息

  • 批准号：
    61572197
  • 项目类别：
    面上项目
  • 资助金额：
    66.0万
  • 负责人：
    蒲戈光
  • 依托单位：
    华东师范大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2019
  • 批准年份：
    2015
  • 项目状态：
    已结题
  • 起止时间：
    2016-01-01 至2019-12-31

项目摘要

Linear Temporal Logic (LTL) plays an important role in the system verification, which is widely used in the model checking and temporal property reasoning for complex systems. This proposal tries to explore the basic theory of LTL and to study the theory, algorithm and application for its satisfiability decision procedure. We would like to exploit the mathematic characteristics for linear temporal logic and to design the new decision procedure, which takes the different way to improve the performance of solvers. The goals of this study include the following aspects: 1)Study the mathematic properties of satisfiable/unsatisfiable trace; 2)Study the new algorithm for LTL satisfiability checking, including how to utilize the SAT solver and machine learning techniques to accelerate the performance; 3)Study the application of LTL satisfiability decision procedure. One is to apply the technique to the run verification field, and the other is to apply the technique to the LTL analysis and verification on finite trace in AI field.
线性时态逻辑（Linear Temporal Logic, LTL）在系统验证中扮演着重要的角色，它被广泛的应用于复杂系统的时态推理与模型检查。本项目面向线性时态逻辑LTL的基础理论，研究LTL的可满足性的判定理论、算法以及潜在的应用。本项目力图深入挖掘线性时态逻辑的数学特征，探索新颖并具有高效性能的可满足性判断过程。本项目的研究目标包括如下三方面:1）研究可满足/不满足无限序列所具有的数学特征，如对于给定的LTL公式，一个无限序列满足/不满足该公式应该具内在特征以及与公式的关系;2）研究LTL可满足判定的新算法，包括利用SAT技术与机器学习技术加速LTL可满足判定过程；3）研究LTL可满足判定在系统测试及人工智能逻辑领域的应用，把基于可满足判定的新算法应用于系统测试的研究，并把该方法学拓展到人工智能领域逻辑的分析过程（如有限迹的线性时态逻辑的分析与验证）。

结项摘要

线性时态逻辑（Linear Temporal Logic, LTL）在系统验证中扮演着重要的角色，它被广泛的应用于复杂系统的时态推理与模型检查领域。本项目面向线性时态逻辑LTL 的基础理论，研究LTL 的可满足性判定理论、算法以及潜在的应用。本项目在三个方面做了深入的研究：..1）LTL的可满足性理论与算法，我们研究了LTL公式本身的数学性质，发现了面向SAT的求解框架，研发了Aalta工具，在典型Benchmarks与国际工具对比，总体性能最优；2）LTL在有限迹下的综合研究，我们是国际上第一个研究了LTL在有限迹下的综合算法，包括安全性与公平性制约下的算法研究，实现了相应的工具；3）面向SAT的模型检查新算法研究，我们发现了一个新的硬件模型检查算法，基于模拟逼近的想法，在实验效果上与主流的验证工具性能相当，形成互补。..研究结果发表在人工智能与形式化方法的重要期刊与杂志，如IJCAI、AAAI、HVC、Formal methods in System Design等。培养了2名博士生，5名硕士生，1名博士后。

项目成果

期刊论文数量（5）
专著数量（0）
科研奖励数量（0）
会议论文数量（10）
专利数量（3）
An explicit transition system construction approach to LTL satisfiability checking
零担可满足性检查的显式转换系统构建方法
  • DOI：
    10.1007/s00165-017-0442-2
  • 发表时间：
    2018
  • 期刊：
    Formal Aspects of Computing
  • 影响因子：
    1
  • 作者：
    Li Jianwen;Zhang Lijun;Zhu Shufang;Pu Geguang;Vardi Moshe Y.;He Jifeng
  • 通讯作者：
    He Jifeng
SAT-based explicit LTL reasoning and its application to satisfiability checking
基于SAT的显式LTL推理及其在可满足性检查中的应用
  • DOI：
    10.1007/s10703-018-00326-5
  • 发表时间：
    2019
  • 期刊：
    Formal Methods in System Design
  • 影响因子：
    0.8
  • 作者：
    Jianwen Li;Shufang Zhu;Geguang Pu;Lijun Zhang;Moshe Y.Vardi
  • 通讯作者：
    Moshe Y.Vardi
Towards backbone computing: A Greedy-Whitening based approach
迈向骨干计算：基于贪婪白化的方法
  • DOI：
    10.3233/aic-180763
  • 发表时间：
    2018
  • 期刊：
    AI Communications
  • 影响因子：
    0.8
  • 作者：
    Yueling Zhang;Min Zhang;Geguang Pu;Fu Song;Jiangwen Li
  • 通讯作者：
    Jiangwen Li
A Survey on Data-Flow Testing
数据流测试调查
  • DOI：
    10.1145/3020266
  • 发表时间：
    2017-03
  • 期刊：
    ACM COMPUTING SURVEYS
  • 影响因子：
    16.6
  • 作者：
    Su Ting;Wu Ke;Miao Weikai;Pu Geguang;He Jifeng;Chen Yuting;Su Zhendong
  • 通讯作者：
    Su Zhendong
Accelerating LTL satisfiability checking by SAT solvers
通过 SAT 求解器加速 LTL 可满足性检查
  • DOI：
    10.1093/logcom/exy013
  • 发表时间：
    2018-09
  • 期刊：
    Journal of Logic and Computation
  • 影响因子：
    0.7
  • 作者：
    Li Jianwen;Pu Geguang;Zhang Lijun;Vardi Moshe Y.;He Jifeng
  • 通讯作者：
    He Jifeng

数据更新时间：{{ 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 }}

其他文献

基于GCL语言的测试用例生成方法
  • DOI：
    --
  • 发表时间：
    --
  • 期刊：
    计算机学报
  • 影响因子：
    --
  • 作者：
    Jeff S;ers;江明月;张娜;蒲戈光
  • 通讯作者：
    蒲戈光
基于Event-B的航天器内存管理系统形式化验证
  • DOI：
    10.13328/j.cnki.jos.005218
  • 发表时间：
    2017
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    乔磊;杨孟飞;谭彦亮;蒲戈光;杨桦
  • 通讯作者：
    杨桦

其他文献

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

AI项目思路

AI技术路线图

蒲戈光的其他基金

Web服务组合语言的语义和验证研究
  • 批准号：
    60603033
  • 批准年份：
    2006
  • 资助金额：
    24.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
客服二维码