EFSMT：一种用于信息物理系统的逻辑框架
计算机科学中的逻辑
2013-06-17 v1
摘要
信息物理系统的设计极具挑战性，因为它包含了对分布式和嵌入式实时系统的分析与综合，这些系统通常以非线性方式控制环境。我们利用 EFSMT 应对这一挑战，EFSMT 是约束条件（包括非线性算术）上命题组合的存在 - 全称量化一阶逻辑片段，作为分析与综合信息物理系统的逻辑框架和基础。我们通过将若干关键的验证与综合问题归约为 EFSMT 问题，展示了 EFSMT 的表达能力。本文中的示例问题包括：通过 BIBO 稳定性进行鲁棒控制综合、非线性控制系统的 Lyapunov 系数求解、用于协调系统组件的分布式优先级综合，以及混合控制系统的综合。我们还提出了一种基于两个 SMT 求解器交互的算法来求解 EFSMT 问题，这两个求解器分别用于处理全称量化和存在量化问题。该算法建立在现代 SMT 求解器常用技术的基础上，并通过反例引导的约束强化将其推广至量词推理。EFSMT 求解器使用 Bernstein 多项式来求解非线性算术约束。
引用
@article{arxiv.1306.3456,
title = {EFSMT: A Logical Framework for Cyber-Physical Systems},
author = {Chih-Hong Cheng and Natarajan Shankar and Harald Ruess and Saddek Bensalem},
journal= {arXiv preprint arXiv:1306.3456},
year = {2013}
}