University of Leicester
Browse

On Well-Separation of GR(1) Specifications

Download (855.91 kB)
conference contribution
posted on 2018-05-30, 11:01 authored by Shahar Maoz, Jan Oliver Ringert
Specifications for reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, consist of assumptions and guarantees. One way a controller may satisfy the specification is by preventing the environment from satisfying the assumptions, without satisfying the guarantees. Although valid this solution is usually undesired and specifications that allow it are called non-well-separated. In this work we investigate non-well-separation in the context of GR(1), an expressive fragment of LTL that enables efficient synthesis. We distinguish different cases of non-well-separation, and compute strategies showing how the environment can be forced to violate its assumptions. Moreover, we show how to find a core, a minimal set of assumptions that lead to non-well-separation, and further extend our work to support past-time LTL and patterns. We implemented our work and evaluated it on 79 specifications. The evaluation shows that non-well-separation is a common problem in specifications and that our tools can be efficiently applied to identify it and its causes.

Funding

JOR acknowledges support from a postdoctoral Minerva Fellowship, funded by the German Federal Ministry for Education and Research. Part of this work was done while SM was on sabbatical as visiting scientist at MIT CSAIL. This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).

History

Citation

Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016), 2016, pp. 362-372

Author affiliation

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

Source

24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Seattle, WA

Version

  • AM (Accepted Manuscript)

Published in

Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016)

Publisher

Association for Computing Machinery (ACM)

isbn

978-1-4503-4218-6

Copyright date

2016

Available date

2018-05-30

Publisher version

https://dl.acm.org/citation.cfm?doid=2950290.2950300

Editors

Zimmermann, T.;ClelandHuang, J.;Su, Z.

Temporal coverage: start date

2016-11-13

Temporal coverage: end date

2016-11-18

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC