面向信息物理系统的数值 LTL 综合

信息物理系统（CPS）是通过传感器和执行器与物理世界交互的系统。在此类系统中，传感器读数代表物理量的度量，且传感器值通常是在有界区间内取值的实数。控制律的实现基于对接收到的传感器值进行的非线性数值计算。综合满足 CPS 特性的控制器给形式化方法研究社区带来了巨大挑战，因为大多数自动控制器综合（LTL 综合）工作仅限于具有少量离散布尔域输入的规范。在本报告中，我们提出了一种新颖的方法来解决上述挑战，以综合 CPS 的控制器。我们的核心方法称为数值 LTL 综合，它通过在 LTL 公式中使用实数输入或输出，并允许在规范中定义多项式约束谓词，从而扩展了 LTL 综合。该综合算法基于处理伪布尔结构的 LTL 综合引擎与测试（反）策略（不）可行性的非线性约束有效性检查器之间的交互。该方法通过开发 LTL 综合模块 G4LTL 和有效性检查器 JBernstein，集成到了 CPS 研究框架 Ptolemy II 中。尽管我们仅针对非线性实数算术理论，但伪布尔综合框架的使用也允许轻松扩展以嵌入更丰富的理论集，从而使该技术适用于更广泛的受众。