• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >TCTL Model Checking of Time Petri Nets
【24h】

TCTL Model Checking of Time Petri Nets

机译：时间陪替氏网的TCTL模型检查

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

摘要

We consider Time Petri Nets (TPN) for which a firing time interval is associated with each transition. State space abstractions for TPN preserving various classes of properties (LTL, CTL and CTL~*) can be computed, in terms of so called state classes. Some methods were proposed to check quantitative timed properties but are not suitable for effective verification of properties of real-life systems. In this article, we consider subscript TCTL for TPN (TPN-TCTL) for which temporal operators are extended with a time interval, specifying a time constraint on the firing sequences. We prove the decidability of TPN-TCTL on bounded TPN and give its theoretical complexity. We propose a zone-based state space abstraction that preserves marking reachability and traces of the TPN. As for Timed Automata (TA), the abstraction may use an over-approximation operator on zones to enforce the termination. A coarser (and efficient) abstraction is then provided and proved exact w.r.t. marking reachability and traces (LTL properties). Finally, we consider a subset of TPN-TCTL properties (TPN-TCTLs) for which it is possible to propose efficient on-the-fly model-checking algorithms. Our approach consists in computing and exploring the zone-based state space abstraction. On a practical point of view, the method is integrated in Romeo [Gardey et al. (2005, Proceedings of 17th International Conference on CAV'05, Vol. 3576 of Lecture Notes in Computer Science, 418-423)], a tool for TPN edition and analysis. In addition to the old features it is now possible to effectively verify a subset of TCTL directly on TPN.
机译：我们考虑时间陪替氏网（TPN），其触发时间间隔与每个过渡相关。可以根据所谓的状态类来计算用于保留各种属性类（TPL，CTL和CTL〜*）的TPN的状态空间抽象。提出了一些方法来检查定量定时属性，但不适用于有效验证实际系统的属性。在本文中，我们考虑TPN的下标TCTL（TPN-TCTL），其时间运算符具有一个时间间隔，并指定了触发序列的时间约束。我们证明了TPN-TCTL在有界TPN上的可判定性，并给出了其理论上的复杂性。我们提出了一种基于区域的状态空间抽象，该抽象保留了标记的可到达性和TPN的痕迹。对于定时自动机（TA），抽象可以在区域上使用过逼近运算符来强制终止。然后提供了一个更粗略（有效）的抽象，并证明了确切的准确率。标记可达性和痕迹（LTL属性）。最后，我们考虑了TPN-TCTL属性（TPN-TCTL）的子集，为此可以提出有效的实时模型检查算法。我们的方法包括计算和探索基于区域的状态空间抽象。从实际的角度来看，该方法已集成在Romeo中[Gardey等。 （2005年，第17届CAV'05国际会议论文集，计算机科学讲义第3576卷，第418-423页）]，一种TPN版本和分析工具。除了旧功能之外，现在还可以直接在TPN上有效地验证TCTL的子集。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号