Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent acceleration techniques have been proposed to address this issue, they often rely on acceleration arguments of limited expressiveness. In this work, we propose an approach for the modular computation of acceleration arguments. It enables the construction of complex acceleration arguments by composing simpler ones, thereby improving both scalability and flexibility. In addition, we introduce a summarization technique that generalizes discovered acceleration arguments, allowing them to be efficiently reused across multiple contexts. Together, these contributions improve the efficiency of solving infinite-state games in reactive synthesis, as demonstrated by our experimental evaluation.

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

Modular Attractor Acceleration in Infinite-State Games

  • Philippe Heim,
  • Rayna Dimitrova

摘要

Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent acceleration techniques have been proposed to address this issue, they often rely on acceleration arguments of limited expressiveness. In this work, we propose an approach for the modular computation of acceleration arguments. It enables the construction of complex acceleration arguments by composing simpler ones, thereby improving both scalability and flexibility. In addition, we introduce a summarization technique that generalizes discovered acceleration arguments, allowing them to be efficiently reused across multiple contexts. Together, these contributions improve the efficiency of solving infinite-state games in reactive synthesis, as demonstrated by our experimental evaluation.