University of Leicester
Browse

Environmentally-Friendly GR(1) Synthesis

Download (680.1 kB)
conference contribution
posted on 2019-06-10, 15:20 authored by Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck
Many problems in reactive synthesis are stated using two formulas—an environment assumption and a system guarantee—and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools often produce strategies that formally satisfy such specifications by actively preventing an environment assumption from holding. While formally correct, such strategies do not capture the intention of the designer. We introduce an additional requirement in reactive synthesis, non-conflictingness, which asks that a system strategy should always allow the environment to fulfill its liveness requirements. We give an algorithm for solving GR(1) synthesis that produces non-conflicting strategies. Our algorithm is given by a 4-nested fixed point in the µ-calculus, in contrast to the usual 3-nested fixed point for GR(1). Our algorithm ensures that, in every environment that satisfies its assumptions on its own, traces of the resulting implementation satisfy both the assumptions and the guarantees. In addition, the asymptotic complexity of our algorithm is the same as that of the usual GR(1) solution. We have implemented our algorithm and show how its performance compares to the usual GR(1) synthesis algorithm.

Funding

N. Piterman—Supported by project “d-SynMA” that is funded by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 772459).

History

Citation

Lecture Notes in Computer Science (LNCS), 2019, 11428 , pp. 229-246

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Informatics

Source

International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2019

Version

  • VoR (Version of Record)

Published in

Lecture Notes in Computer Science (LNCS)

Publisher

Springer Verlag (Germany)

issn

0302-9743

eissn

1611-3349

isbn

9783030174644

Acceptance date

2019-01-26

Copyright date

2019

Available date

2019-06-10

Publisher version

https://link.springer.com/chapter/10.1007/978-3-030-17465-1_13

Book series

Lecture Notes in Computer Science (LNCS );11428

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Keywords

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC