I. Introduction
Reactive systems, such as robot systems, are an architectural style that allows multiple individual applications to blend into one unit, reacting to their environment, while staying aware of each other. Temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. The synthesis of reactive systems from its temporal logic specification is an automated procedure for developing correct-by-construction control software. Two of main challenges in bringing reactive synthesis to software engineering practice are its high worst-case synthesis time and the difficulty of writing specifications because it is difficult to understand. To address the two challenges, Piterman et al. proposed a fragment of LTL named GR(1) which has an efficient polynomial-time symbolic synthesis algorithm [1]. Meanwhile, GR(1) conforms to a simple form, which makes it easier for designers to write specifications.