Scholarlink

<p>In this article, we focus on improving the efficiency of diagnosability checking for real-time systems modeled as timed automata. Inspired by a recently introduced extension of the classic CEGAR (CounterExample-Guided Abstraction Refinement) algorithm, namely the RECAR (Recursive Explore and Check Abstraction Refinement) algorithm, we propose new RECAR-like algorithms that combine over-approximation and under-approximation techniques. We use CEGAR to quickly terminate the refinement loop by over-approximation and under-approximation, in the case where the original formula is respectively satisfiable or unsatisfiable, and then show the soundness of our RECAR-like approach applied to an arbitrary formula. We define then several types of parameterized over- and under-approximations along with refinement strategies for the diagnosability problem. Finally, we evaluate the effectiveness of our method and its implementation with the Z3 SMT solver on different benchmarks by comparing it to the direct method without approximation shortcuts.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

An approximation-based incremental SMT approach for diagnosability analysis of real-time systems

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年8月23日

查看全文
  • Lulu He,
  • Philippe Dague,
  • Lina Ye

摘要

In this article, we focus on improving the efficiency of diagnosability checking for real-time systems modeled as timed automata. Inspired by a recently introduced extension of the classic CEGAR (CounterExample-Guided Abstraction Refinement) algorithm, namely the RECAR (Recursive Explore and Check Abstraction Refinement) algorithm, we propose new RECAR-like algorithms that combine over-approximation and under-approximation techniques. We use CEGAR to quickly terminate the refinement loop by over-approximation and under-approximation, in the case where the original formula is respectively satisfiable or unsatisfiable, and then show the soundness of our RECAR-like approach applied to an arbitrary formula. We define then several types of parameterized over- and under-approximations along with refinement strategies for the diagnosability problem. Finally, we evaluate the effectiveness of our method and its implementation with the Z3 SMT solver on different benchmarks by comparing it to the direct method without approximation shortcuts.