Counter-strategy guided refinement of GR(1) temporal logic specifications
Counter-strategy guided refinement of GR(1) temporal logic specifications
The reactive synthesis problem is to find a finite-state controller that satisfies a given temporal-logic specification regardless of how its environment behaves. Developing a formal specification is a challenging and tedious task and initial specifications are often unrealizable. In many cases, the source of unrealizability is the lack of adequate …