EFSMT: A Logical Framework for Cyber-Physical Systems

TL;DR

EFSMT introduces a logical framework for analyzing and synthesizing cyber-physical systems, enabling the reduction of complex verification problems to a unified formalism with an innovative solver approach.

Contribution

The paper presents EFSMT, a new logical framework for cyber-physical systems, along with a solver algorithm that handles nonlinear and quantified constraints effectively.

Findings

EFSMT can reduce key verification and synthesis problems to its formalism.

The proposed solver employs Bernstein polynomials for nonlinear constraints.

Demonstrated effectiveness on control and hybrid systems problems.

Abstract

The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework and foundation for analyzing and synthesizing cyber-physical systems. We demonstrate the expressiveness of EFSMT by reducing a number of pivotal verification and synthesis problems to EFSMT. Exemplary problems in this paper include synthesis for robust control via BIBO stability, Lyapunov coefficient finding for nonlinear control systems, distributed priority synthesis for orchestrating system components, and synthesis for hybrid control systems. We are also proposing an algorithm for solving EFSMT problems based on the interplay between two SMT solvers for respectively solving universally and existentially quantified problems. This algorithms builds on commonly used techniques in modern SMT solvers, and generalizes them to quantifier reasoning by counterexample-guided constraint strengthening. The EFSMT solver uses Bernstein polynomials for solving nonlinear arithmetic constraints.