CISPA
Browse
cispa_all_3900.pdf (440.14 kB)

Taming Large Bounds in Synthesis from Bounded-Liveness Specifications

Download (440.14 kB)
conference contribution
posted on 2023-11-29, 18:25 authored by Philippe HeimPhilippe Heim, Rayna DimitrovaRayna Dimitrova
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.

History

Preferred Citation

Philippe Heim and Rayna Dimitrova. Taming Large Bounds in Synthesis from Bounded-Liveness Specifications. In: TACAS Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2023.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

TACAS Tools and Algorithms for Construction and Analysis of Systems (TACAS)

Legacy Posted Date

2023-02-09

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3900, title = "Taming Large Bounds in Synthesis from Bounded-Liveness Specifications", author = "Heim, Philippe and Dimitrova, Rayna", booktitle="{TACAS Tools and Algorithms for Construction and Analysis of Systems (TACAS)}", year="2023", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC