CISPA
Browse

File(s) not publicly available

Specification decomposition for reactive synthesis

journal contribution
posted on 2023-11-29, 18:06 authored by Bernd FinkbeinerBernd Finkbeiner, Gideon Geier, Noemi Passing
Reactive synthesis is the task of automatically deriving a correct implementation from a specification. It is a promising technique for the development of verified programs and hardware. Despite recent ad- advances in terms of algorithms and tools, however, re-active synthesis is still not practical when the specified systems reach a certain bound in size and complexity. In this paper, we present a sound and complete modular synthesis algorithm that automatically decomposes the specification into smaller subspecifications. For them, independent synthesis tasks are performed, significantly reducing the complexity of the individual tasks. Our decomposition algorithm guarantees that the subspecifications are independent in the sense that completely separate synthesis tasks can be performed for them. Moreover, the composition of the resulting implementations is guaranteed to satisfy the original specification. Our algorithm is a preprocessing technique that can be applied to a wide range of synthesis tools. We evaluate our approach with state-of-the-art synthesis tools on established benchmarks: the runtime decreases significantly when synthesizing implementations modularly.

History

Preferred Citation

Bernd Finkbeiner, Gideon Geier and Noemi Passing. Specification decomposition for reactive synthesis. In: Innovations in Systems and Software Engineering. 2022.

Primary Research Area

  • Threat Detection and Defenses

Legacy Posted Date

2022-11-08

Journal

Innovations in Systems and Software Engineering

Open Access Type

  • Gold

Sub Type

  • Article

BibTeX

@article{cispa_all_3870, title = "Specification decomposition for reactive synthesis", author = "Finkbeiner, Bernd and Geier, Gideon and Passing, Noemi", journal="{Innovations in Systems and Software Engineering}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC