• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Chinese Journal of Electronics >Quantitative Verification of Knowledge Precondition for Open System
【24h】

Quantitative Verification of Knowledge Precondition for Open System

机译：开放系统知识前提的定量验证

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

A quantitative verification method is proposed to quantitatively verify knowledge precondition of actions and plans. Probability epistemic game structure (PEGS) is proposed to model knowledge preconditions in open systems, an extension of concurrent game structure with probabilistic transition. We introduce a probability operator P-λ into Alternating temporal epistemic logic (ATEL) and define a Probability alternating-time temporal epistemic logic (PATEL) for quantitatively model checking the properties of PEGS. We designed an algorithm to compute the probability aiming at model checking verification problems of PATEL based on DTMC and CTMC. We convert a portion of the PATEL verification problems into PATL problems by defining the knowledge formulas Kaφ, EAsφ and CAsφ as atomic propositions. We study a train controller using PRISM-games to demonstrate the applicability of above quantitative verification method.
机译：提出了一种定量验证方法，以定量验证行动和计划的知识前提。提出了概率认知博弈结构（PEGS），以对开放系统中的知识前提进行建模，这是并发博弈结构具有概率转移的扩展。我们将概率算子P-λ引入交替时间认知逻辑（ATEL），并定义了概率交替时间认知逻辑（PATEL），以对PEGS的性质进行定量模型检查。针对基于DTMC和CTMC的PATEL模型检查验证问题，设计了一种计算概率的算法。通过将知识公式Kaφ，EAsφ和CAsφ定义为原子命题，我们将一部分PATEL验证问题转换为PATL问题。我们研究了使用PRISM游戏的火车控制器，以证明上述定量验证方法的适用性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号