• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual IEEE International Systems Conference >Formalization of Birth-Death and IID processes in higher-order logic
【24h】

Formalization of Birth-Death and IID processes in higher-order logic

机译：出生死亡和IID流程在高阶逻辑中的形式化

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Markov chains are extensively used in the modeling and analysis of engineering and scientific problems. Usually, paper-and-pencil proofs, simulation or computer algebra software are used to analyze Markovian models. However, these techniques either are not scalable or do not guarantee accurate results, which are vital in safety-critical systems. Probabilistic model checking has been proposed to formally analyze Markovian systems, but it suffers from the inherent state-explosion problem and unacceptable long computation times. Higher-order-logic theorem proving has been recently used to overcome the above-mentioned limitations but it lacks any support for discrete Birth-Death process and Independent and Identically Distributed (IID) random process, which are frequently used in many system analysis problems. In this paper, we formalize these notions using formal Discrete-Time Markov Chains (DTMC) with finite state-space and classified DTMCs in higher-order logic theorem proving. To demonstrate the usefulness of the formalizations, we present the formal performance analysis of two software applications.
机译：马尔可夫链广泛用于工程和科学问题的建模和分析。通常，使用纸笔证明，模拟或计算机代数软件来分析马尔可夫模型。但是，这些技术要么不可扩展，要么不能保证准确的结果，这对于安全性至关重要的系统至关重要。已经提出了概率模型检查来正式分析马尔可夫系统，但是它具有固有的状态爆炸问题和难以接受的长计算时间。最近已使用高阶逻辑定理证明来克服上述限制，但它不支持离散的生死过程和独立且完全相同的分布（IID）随机过程，而后者通常在许多系统分析问题中使用。在本文中，我们使用具有有限状态空间和分类DTMC的形式化离散时间马尔可夫链（DTMC）在高阶逻辑定理证明中将这些概念形式化。为了证明形式化的有用性，我们介绍了两个软件应用程序的形式化性能分析。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号