Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis (Full Version)

TL;DR

This paper introduces a novel translation method for temporal logic in infinite-state reactive synthesis, leveraging semantic information to improve the efficiency of game solving.

Contribution

It presents the first approach that constructs monitors with first-order and temporal reasoning, enhancing translation efficiency for infinite-state reactive systems.

Findings

Outperforms state-of-the-art techniques on benchmarks

Enriches game construction with semantic information

Speeds up solving of infinite-state games

Abstract

Infinite-state reactive synthesis has attracted significant attention in recent years, which has led to the emergence of novel symbolic techniques for solving infinite-state games. Temporal logics featuring variables over infinite domains offer an expressive high-level specification language for infinite-state reactive systems. Currently, the only way to translate these temporal logics into symbolic games is by naively encoding the specification to use techniques designed for the Boolean case. An inherent limitation of this approach is that it results in games in which the semantic structure of the temporal and first-order constraints present in the formula is lost. There is a clear need for techniques that leverage this information in the translation process to speed up solving the generated games. In this work, we propose the first approach that addresses this gap. Our technique constructs a monitor incorporating first-order and temporal reasoning at the formula level, enriching the constructed game with semantic information that leads to more efficient solving. We demonstrate that thanks to this, our method outperforms the state-of-the-art techniques across a range of benchmarks.