热带 Fourier-Motzkin 消元法及其在实时验证中的应用

我们引入了一种热带多面体的推广形式，能够表达严格和非严格不等式。此类不等式通过芽 (germs) 半环（编码无穷小扰动）进行处理。我们开发了 Fourier-Motzkin 消元法的热带类比，并由此推导出这些多面体的几何性质。特别是，我们证明了它们等同于在经典意义和热带意义上均凸的（不一定闭合）单元的热带凸并集。我们还证明了在执行连续消元步骤时产生的冗余不等式可以通过归约为平均收益博弈问题进行动态删除。作为补充，我们提供了一种较粗糙（多项式时间）的删除过程，足以使总执行时间达到简单的指数界。这些算法通过其在实时系统（时间自动机的可达性分析）中的应用进行了说明。