Taming Large Bounds in Synthesis from Bounded-Liveness Specifications (Full Version)

TL;DR

This paper introduces a new synthesis method tailored for Safety LTL specifications with large bounded temporal operators, significantly improving efficiency over existing tools for timing-constrained systems.

Contribution

It presents a novel synthesis approach specifically optimized for large bounds in bounded temporal operators within Safety LTL, enhancing performance for timing-critical specifications.

Findings

Outperforms state-of-the-art synthesis tools on large-bound specifications

Efficiently handles quantitative timing constraints in safety specifications

Demonstrates practical viability for large bounds in synthesis problems

Abstract

Automatic synthesis from temporal logic specifications is an attractive alternative to manual system design, due to its ability to generate correct-by-construction implementations from high-level specifications. Due to the high complexity of the synthesis problem, significant research efforts have been directed at developing practically efficient approaches for restricted specification language fragments. In this paper, we focus on the Safety LTL fragment of Linear Temporal Logic (LTL) syntactically extended with bounded temporal operators. We propose a new synthesis approach with the primary motivation to solve efficiently the synthesis problem for specifications with bounded temporal operators, in particular those with large bounds. The experimental evaluation of our method shows that for this type of specifications, it outperforms state-of-art synthesis tools, demonstrating that it is a promising approach to efficiently treating quantitative timing constraints in safety specifications.