ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 12:00 - 12:30 at SUN I - Synthesis Chair(s): Roland Meyer

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 mu-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.

Thu 11 Apr

tacas-2019-papers
10:30 - 12:30: TACAS 2019 - Synthesis at SUN I
Chair(s): Roland MeyerTechnical University of Braunschweig
tacas-2019-papers10:30 - 11:00
Talk
Link to publication
tacas-2019-papers11:00 - 11:30
Talk
Nathalie CauchiUniversity of Oxford, Alessandro AbateUniversity of Oxford
Link to publication
tacas-2019-papers11:30 - 12:00
Talk
Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Vincent BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University
Link to publication
tacas-2019-papers12:00 - 12:30
Talk
Link to publication