线性动力系统中极限正性的稳健实例的表征
摘要：线性动态系统，包括离散和连续系统，在诸多应用领域中是非常有价值的数学模型，例如概率系统验证、模型检验、计算生物学、网络物理系统和经济学。我们考虑离散线性递归序列和连续的C-有限函数，即齐次线性微分方程的解。终极正性问题给出递归关系和初始化作为输入，并询问是否存在步长$n_0$（或时间$t_0$），使得线性递归序列$u[n] \geq 0$对于$n > n_0$（或齐次线性微分方程的解$u(t) \geq 0$对于$t > t_0$）。为了解决这些问题，需要克服固有的数论挑战，这在工程和实际科学中至关重要。在这些情况下，困难的边界情况很少相关：对固有不精确性的容忍是特别关键的。因此，我们对终极正性问题的「鲁棒」实例进行了特征化，即决策在局部上是恒定的输入。我们使用实数一阶理论描述了鲁棒YES和鲁棒NO实例的集合。我们通过实数一阶理论的限量消除，证明了这些集合是半代数的。
作者：Mihir Vahanwala
论文ID：2308.06421
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-15