...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Information and computation >Complexity analysis of a unifying algorithm for model checking interval temporal logic
【24h】

Complexity analysis of a unifying algorithm for model checking interval temporal logic

机译：模型检查间隔时间逻辑统一算法的复杂性分析

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

摘要

Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently shown to be decidable. An intriguing open question is its exact complexity for full HS: it is at least EXPSPACE-hard, and the only known upper bound, which exploits an abstract representation of Kripke structure paths (descriptor), is non-elementary. In this paper, we provide a uniform framework to MC for full HS and meaningful fragments of it, with a specific type of descriptor for each fragment. Then, we devise a general MC alternating algorithm, parameterized by the descriptor's type, which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze its complexity and give tight bounds on the length of certificates. For two types of descriptor, we obtain exponential upper and lower bounds; for the other ones, we provide non-elementary lower bounds.
机译：最近已显示HALPERN和SHOHAM间隔时间逻辑HS的模型检查（MC）是可判定的。 一个有趣的开放问题是其完全HS的精确复杂性：它至少是expspace - 硬，并且唯一已知的上限，它利用kripke结构路径的抽象表示（描述符），是非基本的。 在本文中，我们为MC提供了一个统一的框架，用于全HS和它的有意义的片段，每个片段都有特定类型的描述符。 然后，我们设计了一般的MC交替算法，由描述符的类型参数化，其具有多项式有界数的交替，并且其运行时间由描述符的最小代表的长度（证书）界定。 我们分析其复杂性，并在证书的长度上给出紧张的界限。 对于两种类型的描述符，我们获得指数上限和下限; 对于另一个，我们提供非基本下限。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号