线性算术中整数和实数变量的有效决策过程
摘要：有限自动机算法用于处理具有实数和整数变量的线性算术的这篇论文。之前的研究表明，可以通过使用无限字上的有限自动机来处理这个理论，但这涉及到一些难以实现的困难和精巧的算法。本文的贡献是通过使用拓扑论的论证，展示仅需要一类有限自动机来处理实数和整数线性算术。这使得可以使用更简单的算法，已经成功实施。
作者：Bernard Boigelot, Sebastien Jodogne and Pierre Wolper
论文ID：cs/0303019
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23