位置：成果数据库 > 期刊 > 期刊详情页
有界模型检测同步多智体系统的时态认知逻辑
  • ISSN号：1000-9825
  • 期刊名称：《软件学报》
  • 时间：0
  • 分类：TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构：[1]桂林电子科技大学计算机系,广西桂林541004, [2]中山大学计算机科学系,广东广州510275, [3]河南科技大学电子信息工程学院,河南洛阳471003
  • 相关基金：Supported by the National Natural Science Foundation of China under Grant Nos.60496327. 10410638, 60473004 （国家自然科学基金）; the National Grand Fundamental Research 973 Program of China under Grant No.2005CB321900 （国家重点基础研究发展规划（973））; the Natural Science Foundation of Guangdong Province of China under Grant Nos.04205407.（广东省自然科学基金）
作者： 骆翔宇[1,2], 苏开乐[2,3], 杨晋吉[2]
关键词： 模型检测, 有界模型检测, 多智体系统, 同步时态认知模型, 时态认知逻辑, model checking, bounded model checking, multi-Agent system, synchronous temporal epistemic model, temporal epistemic logic
中文摘要：

提出在同步的多智体系统中验证时态认知逻辑的有界模型检测（bounded model checking，简称BMC）算法．基于同步解释系统语义，在时态逻辑CTL＊的语言中引入认知模态词，从而得到一个新的时态认知逻辑ECKLn通过引入状态位置函数的方法获得同步系统的智能体知识，避免了为时问域而扩展通常的时态认知模型的状态及迁移关系编码．ECKLn的时态认知表达能力强于另一个逻辑CTLKn给出该算法的技术细节及正确性证明。并用火车控制系统实例解释算法的执行过程．

英文摘要：

This paper presents an approach to the verification of temporal epistemic logic in synchronous multi-Agent systems via bounded model checking （BMC）. By incorporating epistemic modalities into temporal logic CTL＊, a temporal epistemic logic ECKLn is introduced, and it is interpreted under the semantics of synchronous interpreted system. The temporal epistemic expressive power of ECKLn is greater than that of Penczek and Lomuscio＇s logic CTLK. Agents＇ knowledge interpreted under synchronous semantics can be skillfully attained by the state position function, which avoids extending the encoding of the states and the transition relation of plain temporal epistemic model for time domain. The technical details and the correctness of the BMC method for logic AECKLn/EECKLn （the universal or existential fragment of ECKLn） are given. A case study of train controller system is presented to illustrate the processing of the BMC method,

同期刊论文项目
非规范知识交叉领域研究
期刊论文 134 会议论文 68 著作 2
　海量信息的协同性和可生存性的理论与实践研究
期刊论文 4
系统规范表示与验证的认识逻辑途径
期刊论文 64 会议论文 33 著作 2
同项目期刊论文
Missing is Useful": Missing Values in Cost-sensitive Decision Trees
Computation of Arbitrage in Frictional Bond Markets
Optimal Dynamic Portfolio Selection with Earnings-at-Risk
Compensatory ability to null mutation in metabolic networks
An Effective GML Documents Compressor
Random Sierpinski network with scale-free small world and modular structure
Rigorous solution of average distance for Sierpinski network
A Characterization Theorem for Injective Model Classes Axiomatized by General Rules
Similarity between preferential models
Some Representation Theorems for recovering contraction relations
A Simplicial Approach for Discrete Fixed Point Theorems
Computation of Arbitrage in a Financial Market with Various Types of Frictions
An ontology-theme-based method of acquiring knowledge from Chinese natural language documents
A Survey on Description Logic
Prediction of protein-protein interactions from primary sequences
一个基于智能的MAS模型及其方法论
SET证书申请协议在SPV下的自动化验证及改进
多主体系统时态认知规范的"On the fly"模型检测算法研究
有界模型检测同步多智能体系统的时态认知逻辑
有缺指派下的信念修正逻辑
Analog-Cell：一种新的电子细胞图形模型
LIGHT: A Query-Efficient yet Low-Maintenance Indexing Scheme over DHTs
Effects of accelerating growth on the evolution of weighted complex networks
“理解”论：信息内容认知机理的假说
机制主义方法与人工智能统一理论
基于分形技术的数据流突变检测算法
Semantic interpretation of Compositional Logic in Instantiation Space
Mining Multiple Data Sources: Local Pattern Analysis
Detecting Differences between Contrast Groups
Missing Data Analysis: A Kernel-Based Multi-imputation Approach
Cognitive Approach to Artificial Intelligence
Forward Looking Nash Equilibrium for Keyword Auction
Knowledge structure approach to verification of authentication protocols
To build a Blocklist Based on the Cost of Spam
Detecting Inconsistency in Biological Molecular Databases using Ontology
Domain-Driven Data Mining, a Practical Methodology
基于约束的自然语言问题到OWL的语义映射方法研究
Two Representation Theorems for Nonmonotonic Inference Relations
A modal characterization of Lambda-bisimilarity
An algebraic Characterization of equivalent preferential models
符号化模型检测CTL*
论“信息-知识-智能转换规律”
Evolving pseudofractal networks
From regular to growing small-world networks
Computing the Minimum-Support for Mining Frequent Patterns
Identifying Follow Correlation Itemset-Pairs
Estimating Confidence Intervals for Structural Differences between Contrast Groups with Missing Data
Mining Class-bridge Rules Based on Rough Sets
Strategies for Complex Data Cube Queries
Rule-based Dependency Models for Security Protocol Analysis
POP Algorithm: Kernel-Based Imputation to Treat Missing Values in Knowledge Discovery from Databases
Empirical Likelihood Confidence Intervals for Differences between Two Datasets with Missing Data
Activity Mining: from Activities to Actions
Structuralism? Functionalism? Behaviorism? Or Mechanism? - - Looking Backward and Forward for Bett
An Investigation on The Theory of Information-Knowledge-Intelligence Transforms
SAT问题中局部搜索法的改进
Verification of Authentication Protocols for Epistemic Goals via SAT Compilation
Primitive Recursiveness of Real Numbers under Different Representations
Observation-Based Logic of Knowledge, Belief, Desire and Intention.
Primitive recursive real numbers.
Customer Retention: Identifying Actionable Information from Web-Logs
Generalized Dimension-Reduction Framework for Recent-Biased Time Series Analysis
EDUA: An Efficient Algorithm for Dynamic Database Mining
A Behavioural Pseudometric based on lambda—Bisimilarity
On Default Correlation and Pricing of Collateralized Debt Obligation by Copula Functions
Genetic-algorithm-based Strategy for Identifying Association Rules without Specifying Actual Minimum
Self-similarity, small-world, scale-free scaling, disassortativity, and robustness in hierarchical l
A geometric growth model interpolating between regular and small-world networks
Advanced Intelligence and Mechanism Approach
Adaptive indexing for content-based search in P2P systems
Identifying quality knowledge from different data sources
Model Checking Temporal Logics of Knowledge Via OBDDs
知识的内涵与度量
人工智能理论：从分立到统一的奥秘
人工智能：由分立走向和谐
An efficient peer-to-peer indexing tree structure for multidimensional data
Association-Based Segmentation for Chinese-Crossed Query Expansion
On Data Structures for Association Rule Discovery
Tracking clusters in evolving data streams over sliding windows
多智能体系统时态认知规范高效符号模型检测的算法研究
Recursive weighted treelike networks
一种支持多维数据范围查询的对等计算索引框架
Characterize branching distance in terms of ()-bisimilarity
非结构化对等计算系统中多维范围搜索
信息转换原理：信息、知识、智能的一体化理论
一种多特征方查询的有效算法
一种有效的信息检索模型
完全加权关联规则挖掘及其在查询扩展中的应用
多数据库中例外模式挖掘方法研究
关系数据库中基于区域聚类的多区域查询优化
复杂网络研究进展：模型与应用
使用SVMs进行汉语浅层分析
注意-情绪协调的个性化信息推荐模型
目的地选择服务系统中的智能逻辑推理
语言认知与主题内容识别
移动个性化信息服务中的用户兴趣模型
鲁棒局部保持投影的表情识别
基于全信息自然语言理解的语音识别后文本处理
基于实例的机器辅助写作翻译系统
信任感知的组合服务动态选择方法
基于高维空间的在线高效子空间Skyline算法——CSky
用CLP技术解决动画自动生成中的布局规划问题
谱聚类算法对输入数据顺序的敏感性
短信过滤系统设计分析
数据流中概念漂移检测的集成分类器设计
实例化空间：一种新的安全协议验证逻辑的语义模型
多主体系统时态认知规范的“On the Fly”模型检测算法研究
智能目的地选择服务系统的设计与实现
基于图形处理器的数据流快速聚类
基于滑动窗口的进化数据流聚类
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
一种改进的基于规则的带权模糊推理算法
Quantum software framework： a tentative study
相对时钟倾斜的相干检测算法
期刊信息
  • 《软件学报》
  • 北大核心期刊（2011版）
  • 主管单位:中国科学院
  • 主办单位:中国科学院软件研究所 中国计算机学会
  • 主编：赵琛
  • 地址：北京8718信箱中国科学院软件研究所
  • 邮编：100190
  • 邮箱：jos@iscas.ac.cn
  • 电话：010-62562563
  • 国际标准刊号：ISSN：1000-9825
  • 国内统一刊号：ISSN：11-2560/TP
  • 邮发代号:82-367
  • 获奖情况:
  • 2001年入选中国期刊方阵“双百期刊”,2000年荣获中国科学院优秀科技期刊一等奖
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国数学评论（网络版）,波兰哥白尼索引,德国数学文摘,荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊（2004版）,中国北大核心期刊（2008版）,中国北大核心期刊（2011版）,中国北大核心期刊（2014版）,中国北大核心期刊（2000版）
  • 被引量:54609