Numerical LTL Synthesis for Cyber-Physical Systems
This work addresses the problem of controller synthesis for cyber-physical systems, enabling formal methods to handle continuous real-world data, though it is incremental as it builds on existing LTL synthesis techniques.
The authors tackled the challenge of synthesizing controllers for cyber-physical systems (CPS) with real-valued sensor inputs and nonlinear computations, which existing LTL synthesis methods cannot handle due to their restriction to discrete Boolean domains. They developed a numerical LTL synthesis approach that extends LTL synthesis to include real numbers and polynomial constraints, resulting in a method integrated into the Ptolemy II framework with modules G4LTL and JBernstein.
Cyber-physical systems (CPS) are systems that interact with the physical world via sensors and actuators. In such a system, the reading of a sensor represents measures of a physical quantity, and sensor values are often reals ranged over bounded intervals. The implementation of control laws is based on nonlinear numerical computations over the received sensor values. Synthesizing controllers fulfilling features within CPS brings a huge challenge to the research community in formal methods, as most of the works in automatic controller synthesis (LTL synthesis) are restricted to specifications having a few discrete inputs within the Boolean domain. In this report, we present a novel approach that addresses the above challenge to synthesize controllers for CPS. Our core methodology, called numerical LTL synthesis, extends LTL synthesis by using inputs or outputs in real numbers and by allowing predicates of polynomial constraints to be defined within an LTL formula as specification. The synthesis algorithm is based on an interplay between an LTL synthesis engine which handles the pseudo-Boolean structure, together with a nonlinear constraint validity checker which tests the (in)feasibility of a (counter-)strategy. The methodology is integrated within the CPS research framework Ptolemy II via the development of an LTL synthesis module G4LTL and a validity checker JBernstein. Although we only target the theory of nonlinear real arithmetic, the use of pseudo-Boolean synthesis framework also allows an easy extension to embed a richer set of theories, making the technique applicable to a much broader audience.