CISPA
Browse

Information Flow Guided Synthesis

Download (414.9 kB)
conference contribution
posted on 2023-11-29, 18:20 authored by Bernd FinkbeinerBernd Finkbeiner, Niklas MetzgerNiklas Metzger, Yoram Moses
Compositional synthesis relies on the discovery of assumptions, i.e., restrictions on the behavior of the remainder of the system that allow a component to realize its specification. In order to avoid losing valid solutions, these assumptions should be necessary conditions for realizability. However, because there are typically many different behaviors that realize the same specification, necessary behavioral restrictions often do not exist. In this paper, we introduce a new class of assumptions for compositional synthesis, which we call information flow assumptions. Such assumptions capture an essential aspect of distributed computing, because components often need to act upon information that is available only in other components. The presence of a certain flow of information is therefore often a necessary requirement, while the actual behavior that establishes the information flow is unconstrained. In contrast to behavioral assumptions, which are properties of individual computation traces, information flow assumptions are hyperproperties, i.e., properties of sets of traces. We present a method for the automatic derivation of information-flow assumptions from a temporal logic specification of the system. We then provide a technique for the automatic synthesis of component implementations based on information flow assumptions. This provides a new compositional approach to the synthesis of distributed systems. We report on encouraging first experiments with the approach, carried out with the BoSyHyper synthesis tool.

History

Preferred Citation

Bernd Finkbeiner, Niklas Metzger and Yoram Moses. Information Flow Guided Synthesis. In: Computer Aided Verification (CAV). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date

2022-05-09

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3680, title = "Information Flow Guided Synthesis", author = "Finkbeiner, Bernd and Metzger, Niklas and Moses, Yoram", booktitle="{Computer Aided Verification (CAV)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC