• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Concurrency Theory(CONCUR 2004); 20040831-20040903; London; GB >Model Checking Timed Automata with One or Two Clocks
【24h】

Model Checking Timed Automata with One or Two Clocks

机译：具有一个或两个时钟的模型检查定时自动机

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

摘要

In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL_(≤ , ≥) over TAs with one clock or two clocks. First we show that the reachability problem is NLOGSPACE-comp-lete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL_(≤ , ≥) over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.
机译：在本文中，我们研究了定时自动机（TA）的模型检查，更准确地说，我们的目标是为TA的子类找到有效的模型检查。为此，我们考虑使用一个时钟或两个时钟对TA上的TCTL和TCTL_（≤，≥）进行模型检查。首先，我们证明了一个时钟TA的可达性问题是NLOGSPACE完全完成（即与经典图中的可达性一样复杂），并给出了用于此类TA的模型检查TCTL_（≤，≥）的多项式时间算法。其次，我们表明，对于一个时钟TA上的完整TCTL，模型检查变为PSPACE-complete。我们还显示，在两个时钟TA上的模型检查CTL（无任何时序约束）是PSPACE完整的，并且可达性是NP困难的。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号