首页> 外文会议>IEEE International Symposium on Theoretical Aspects of Software Engineering >Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic
【24h】

Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic

机译:用定时计算树逻辑检查矩形混合系统的模型

获取原文

摘要

To deal with the model checking issue of rectangular hybrid systems, a constraint system called hybrid zone is introduced for the representation and manipulation of rectangular hybrid automata state-spaces. Model checking procedures for rectangular hybrid systems based on timed computation tree logic are given. The hybrid zone is proved to be closed to the operations required in these model checking procedures, which enables it to be used as the basis for the infinite state-space exploring of rectangular hybrid automata. To represent hybrid zones, a data structure difference constraint matrix is introduced.
机译:为了处理矩形混合系统的模型检查问题,引入了一个称为混合区域的约束系统,用于矩形混合自动机状态空间的表示和操纵。给出了基于定时计算树逻辑的矩形混合系统的模型检查过程。证明混合带关闭了这些模型检查程序所需的操作,这使得它能够用作矩形混合自动机的无限状态空间探索的基础。为了表示混合区域,介绍了数据结构差约束矩阵。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号