• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>13th International Conference on CONCUR 2002 - Concurrency Theory, Aug 20-23, 2002, Brno, Czech Republic >A Decidable Fixpoint Logic for Time-Outs
【24h】

A Decidable Fixpoint Logic for Time-Outs

机译：可确定的超时定点逻辑

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

摘要

We show decidability of the satisfiability problem for an extension of the modal μ-calculus with event-recording clocks. Based on techniques for deciding the untimed μ-calculus, we present a complete set of reduction rules for constructing tableaux for formulas of this event-recording logic. To keep track of the actual value of the clocks, the premises and conclusions of our tableau rules are augmented with timing contexts, which are sets of timing constraints satisfied by the actual value of the clocks. The decidability problem is shown to be EXPTIME complete. In addition, we address the problem of model synthesis, that is, given a formula φ, we construct an event-recording automaton that satisfies φ.
机译：我们显示了可扩展性μ演算与事件记录时钟的扩展的可满足性问题的可判定性。基于确定非定时μ演算的技术，我们提供了一套完整的归约规则，用于为该事件记录逻辑的公式构造表格。为了跟踪时钟的实际值，我们的制表规则的前提和结论都增加了定时上下文，这些上下文是时钟的实际值满足的一组定时约束。可判定性问题显示已完成EXPTIME。另外，我们解决了模型综合的问题，即给定公式φ，我们构造了一个满足φ的事件记录自动机。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号