位置：立项数据库 > 立项详情页
系统规范表示与验证的认识逻辑途径
  • 项目名称：系统规范表示与验证的认识逻辑途径
  • 项目类别：面上项目
  • 批准号：60473004
  • 申请代码：F0201
  • 项目来源：国家自然科学基金
  • 研究期限：2005-01-01-2007-12-31
  • 项目负责人：苏开乐
  • 负责人职称：教授
  • 依托单位：中山大学
  • 批准年度：2004
中文摘要：

本课题从分布式系统设计中的规范表示及其形式化验证的需要出发，研究多智能体的认识逻辑的模型检测技术。?围绕知识和信念的表示和建模，我们将提出新型实用的Kripke语义模型。我们也将考虑基于所提出的Kripke语义模型的知识融合和更新问题，并探讨它们与模型检测问题的关系。作为本课题的具体应用，拟开展基于认识逻辑的安全协议验证的模型检测方法研究。对于分布式系统（或多智能体系统），总体来说，还没有在规范表示与形式化验证两方面都令人满意的知识逻辑模型可以使用。本课题将试图通过有认识逻辑的基础理论和关键技术的研究，提出和实现新的知识逻辑模型及其相关算法，从而有可能在系统规范及其验证的研究方面取得实质性进展。

中文主题词： 模型检测多智能体逻辑；极大可满足性问题；安全协议验证
结论摘要：

英文主题词model checking logics of multi-agent systems; Max-SAT problem; verification of security protocols

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 64
  • 33
  • 0
  • 0
  • 2
期刊论文
SAT 问题中局部搜索法的改进
A logical framework for Identifying quality knowledge from different data sources
多主体系统时态认知规范的"On the fly"模型检测算法研究
实例化空间: 一种新的安全协议验证逻辑的语义模型
有界模型检测的优化
SET证书申请协议在SPV下的自动化
多智能体系统时态认知规范高效符
多主体系统时态认知规范的"On th
Bounded model Checking knowled
Computationally grounded model
Improving Encoding Efficiency
MCTK（认识逻辑模型检测工具）
SPV（安全协议分析器）
Verification of Multi-agent Sy
Exploiting Inference Rules to
Within-problem Learning for Ef
BDDRPA*: An Efficient BDD-base
An Extended Interpreted System
一个基于智能的 MAS 模型及其方法论
Primitive Recursive Real Numbers under different Representations
Primitive Recursive Real Numbers
SET 证书申请协议在 SPV 下的自动化验证及改进
一个基于智能的MAS模型及其方法论
SET证书申请协议在SPV下的自动化验证及改进
Verification of Authentication Protocols for Epistemic Goals via SAT Compilation
Knowledge structure approach t
实例化空间: 一种新的安全协议验
基于知识结构的认证协议验证
符号化模型检测CTL
多智能体系统时态认知规范的"On
Identifying quality knowledge
一个基于智能的MAS模型及其方法
Model Checking Temporal Logics
Semantic interpretation of Com
有界模型检测同步多智能体系统的
Verification of Authentication
Primitive Recursive Real Numbe
实例化空间：一种新的安全协议验证逻辑的语义模型
多主体系统时态认知规范的“On the Fly”模型检测算法研究
有界模型检测同步多智体系统的时态认知逻辑
一种基于多模式加密算法的文件保护方案
网络课程中基于Web的在线测试系统的研究与实现
New Retrieval Method Based on Relative Entropy for Language Modeling with Different Smoothing Methods
会议论文
The Interpreted System Model of Knowledge, Belief, Desire and Intention
BDDRPA*: An Efficient BDD-based Incremental Heuristic Search Algorithm For Replanning
Verification of Multi-agent Systems via Bounded Model Checking
Reasoning About Knowledge by SAT Solving
Observation-Based Logic of Knowledge, Belief, Desire and Intention
Exploiting Inference Rules to Compute Lower Bounds for MAX-SAT Solving
Computationally grounded model of BDI-agents
A theory of forgetting in logic programming
Formal Analysis and Improvement of the State Transition Model for Intrusion Tolerant System
Model Checking Temporal Logics of Knowledge and Its Application in Security Verification
Primitive Recursive Real Numbe
Observation-based model for BD
The Algorithm Research for On
Observation-based model for BDI-agents
A Computationally Grounded Logic of Knowledge, Belief and Certainty
Bounded model Checking knowledge and branching time in synchronous multi-agent systems
Observation-Based Logic of Kno
A theory of forgetting in logi
Reasoning About Knowledge by S
A Computationally Grounded Log
The Interpreted System Model o
Model Checking Temporal Logics
Improving Encoding Efficiency for Bounded Model Checking
Observation-Based Logic of Kno
A theory of forgetting in logi
Within-problem Learning for Efficient Lower Bound Computation in Max-SAT Solving
Reasoning About Knowledge by S
Model Checking Temporal Logics
Observation-based model for BD
A Modal Logic for Beliefs and Pro Attitudes
A Computationally Grounded Log
The Interpreted System Model o
An Extended Interpreted System Model for Epistemic Logics
著作
Primitive Recursive Real Numbe
Formal Analysis and Improvemen
苏开乐的项目
认识逻辑及其在安全协议设计、验证中的应用
期刊论文 14 会议论文 5
若干典型的非单调逻辑的比较研究
期刊论文 7