Numerical LTL Synthesis for Cyber-Physical Systems

TL;DR

This paper introduces a novel numerical LTL synthesis approach for cyber-physical systems, enabling controller synthesis with real-valued inputs and polynomial constraints, bridging a gap in formal methods for CPS.

Contribution

It extends LTL synthesis to handle real-valued inputs and polynomial constraints, integrating nonlinear real arithmetic into controller synthesis for CPS.

Findings

Developed a new numerical LTL synthesis methodology.

Implemented the approach within the Ptolemy II framework.

Demonstrated the method's applicability to CPS control problems.

Abstract

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.