Taming Large Bounds in Synthesis from Bounded-Liveness Specifications

(2023) Taming Large Bounds in Synthesis from Bounded-Liveness Specifications. (In Press)

Text paper_131.pdf Download (450kB)

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.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Rayna Dimitrova (RD)
Conference:	TACAS Tools and Algorithms for Construction and Analysis of Systems
Depositing User:	Rayna Dimitrova
Date Deposited:	09 Feb 2023 13:32
Last Modified:	09 Feb 2023 13:32
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/3900

Actions

Actions (login required)

View Item