• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Formal description techniques IX : Theory, application and tools >Time - action alternating model for timed LOTOS and its symbolic verification of bisimulation equivalence
【24h】

Time - action alternating model for timed LOTOS and its symbolic verification of bisimulation equivalence

机译：定时LOTOS的时间-动作交替模型及其双仿真等价性的符号验证。

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

摘要

Verification of timed bisimulation equivalence is generally difficult because of state explosion caused by concrete time values. In this paper, we propose a verification method to verify timed bisimulation equivalence of two timed processes using a symbolic technique similar to (Hennessy and Lin 1995). We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In A-TSLTS, each state has some parameter variables and those values determine its behaviour. Each transition in an A-TSLTS has a guard predicate. The transition is executable if and only if its guard predicate is true under specified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS to make the state-pair be timed bisimulation equivalent. We also show that this result can be applied to the language LOTOS/T(Nakata et al. 1994), a timed extension of LOTOS (ISO 1989).
机译：由于具体时间值导致状态爆炸，因此很难对定时双仿真等效性进行验证。在本文中，我们提出了一种验证方法，使用类似于（Hennessy and Lin 1995）的符号技术来验证两个定时过程的定时双仿真等效性。我们首先提出一种定时过程的新模型，即交替定时符号标记转换系统（A-TSLTS）。在A-TSLTS中，每个状态都有一些参数变量，这些值决定其行为。 A-TSLTS中的每个转换都有一个保护谓词。当且仅当在指定参数值下其保护谓词为true时，转换才可执行。在提出的方法中，我们可以在有限的A-TSLTS中获得状态对的最弱条件，以使状态对在定时双仿真中等效。我们还表明，该结果可以应用于LOTOS / T语言（Nakata等，1994），是LOTOS的定时扩展（ISO 1989）。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号