CISPA
Browse
cispa_all_3871.pdf (687.84 kB)

Synthesizing Dominant Strategies for Liveness

Download (687.84 kB)
conference contribution
posted on 2023-11-29, 18:25 authored by Bernd FinkbeinerBernd Finkbeiner, Noemi Passing
Reactive synthesis automatically derives a strategy that satisfies a given specification. However, requiring a strategy to meet the specification in every situation is, in many cases, too hard of a requirement. Particularly in compositional synthesis of distributed systems, individual winning strategies for the processes often do not exist. Remorsefree dominance, a weaker notion than winning, accounts for such situations: dominant strategies are only required to be as good as any alternative strategy, i.e., they are allowed to violate the specification if no other strategy would have satisfied it in the same situation. The composition of dominant strategies is only guaranteed to be dominant for safety properties, though; preventing the use of dominance in compositional synthesis for liveness specifications. Yet, safety properties are often not expressive enough. In this paper, we thus introduce a new winning condition for strategies, called delay-dominance, that overcomes this weakness of remorsefree dominance: we show that it is compositional for both safety and liveness specifications, enabling a compositional synthesis algorithm based on delay-dominance for general specifications. Furthermore, we introduce an automaton construction for recognizing delay-dominant strategies and prove its soundness and completeness. The resulting automaton is of single-exponential size in the squared length of the specification and can immediately be used for safraless synthesis procedures. Thus, synthesis of delay-dominant strategies is, as synthesis of winning strategies, in 2EXPTIME.

History

Preferred Citation

Bernd Finkbeiner and Noemi Passing. Synthesizing Dominant Strategies for Liveness. In: Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 2022.

Primary Research Area

  • Threat Detection and Defenses

Name of Conference

Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

Legacy Posted Date

2022-11-08

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3871, title = "Synthesizing Dominant Strategies for Liveness", author = "Finkbeiner, Bernd and Passing, Noemi", booktitle="{Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC