EFSMT：信息物理系统的逻辑框架
EFSMT: A Logical Framework for Cyber-Physical Systems
摘要：
信息物理系统的设计是具有挑战性的，因为它包括分布式和嵌入式实时系统的分析和综合，通常以非线性的方式控制环境。我们解决这一挑战与EFSMT，存在的所有量化的命题组合的一阶片段的约束（包括非线性算术），作为逻辑框架和基础，分析和合成网络物理系统。我们证明了EFSMT的表现力，减少了一些关键的验证和综合问题，EFSMT。本文中的示例性问题包括通过BIBO稳定性的鲁棒控制合成，非线性控制系统的李雅普诺夫系数发现，分布式优先级合成编排系统组件，和混合控制系统的合成。我们还提出了一个算法，解决EFSMT问题的基础上，两个SMT求解器之间的相互作用，分别解决普遍和存在的量化问题。该算法建立在现代SMT求解器中常用的技术基础上，并通过反例引导的约束增强将其推广到量词推理。EFSMT求解器使用Bernstein多项式来求解非线性算术约束。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
