Presburger算术中自动机大小的界限
摘要：普雷斯伯格算术的决策过程由自动机提供。然而，到目前为止，关于该方法产生的自动机大小只知道粗糙的下界和上界。在本文中，我们证明了普雷斯伯格算术公式的最小确定性自动机的状态数量的上界。这个上界取决于公式的长度和公式中出现的量词。通过将普雷斯伯格算术公式的自动机与量词消除方法产生的公式进行比较，建立了这个上界。我们还证明了即使对于非确定性自动机，我们的上界也是紧密的。此外，我们提供了线性方程和不等式的最优自动机构造方法。
作者：Felix Klaedtke
论文ID：cs/0506008
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23