Polynomial-Time Algorithm for Realizing Expressive Temporal Logic Specifications

The authors present a polynomial-time algorithm for deciding realizability of the expressive GXU sublogic of linear temporal logic, which is suitable for specifying embedded control systems. The algorithm reduces realizability to solving a certain subclass of 2QBF satisfiability problems.