The last few years have seen a rising interest in the problem of synthesizing systems from temporal logic specifications. One major contributor to this is the recent work of Piterman et al., which showed how polynomial time synthesis could be achieved for a class of LTL specifications that is large enough and expressive enough to cover an extensive number of complex, real-world, applications (despite a known doubly-exponential time lower bound for general LTL formulae). That approach has already been used extensively for the synthesis of various applications and as basis for further theoretical work on synthesis. Here, we expose a fundamental flaw in the initial processing of specifications in that paper and demonstrate how it may produce incorrect results, declaring that specifications could not be synthesized when, in fact, they could. We then identify a class of specifications for which this initial processing is sound and complete. Thus, giving an insight to the reason that this problem arises in the first place. We also show that it can be easily checked whether specifications belong to the sound and complete class by using the same synthesis techniques. Finally, we show in the cases that specifications do not fall into this category how to modify them so that their processing is, indeed, both sound and complete. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Klein, U., & Pnueli, A. (2011). Revisiting synthesis of GR(1) specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6504 LNCS, pp. 161–181). https://doi.org/10.1007/978-3-642-19583-9_16
Mendeley helps you to discover research relevant for your work.