Structural Synthesis for GXW Specifications

Abstract

We define the \(\textsf {\small {GXW}} \) fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since \(\textsf {\small {GXW}} \) includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For \(\textsf {\small {GXW}} \) controller specifications, we develop a novel approach for synthesizing a set of synchronously communicating actor-based controllers. This synthesis algorithm proceeds by means of recursing over the structure of \(\textsf {\small {GXW}} \) specifications, and generates a set of dedicated and synchronously communicating sub-controllers according to the formula structure. In a subsequent step, 2QBF constraint solving identifies and tries to resolve potential conflicts between individual \(\textsf {\small {GXW}} \) specifications. This structural approach to \(\textsf {\small {GXW}} \) synthesis supports traceability between requirements and the generated control code as mandated by certification regimes for safety-critical software. Our experimental results suggest that GXW synthesis scales well to industrial-sized control synthesis problems with 20 input and output ports and beyond.