逆向方法实现了模态可满足性的自动机方法
摘要：基于表格的决策过程面对模态逻辑和描述逻辑的可满足性表现良好，但是在使用这些方法中有时很难获得精确的最坏情况复杂度结果，特别是对于EXPTIME完备的逻辑。相比之下，基于自动机的方法通常能够产生可以轻松证明最优最坏情况复杂度的算法。然而，这种方式获得的算法通常不仅是最坏情况下，而且还是最好情况下的指数级：它们首先构造一个与输入大小成指数关系的自动机，然后对这个大型自动机应用（多项式时间的）是否为空的测试。为了克服这个问题，必须在执行是否为空测试时“即时”构造自动机。本文将展示Voronkov针对模态逻辑K的逆向方法可以被视为自动机方法对K进行是否为空测试的即时实现。这个结果的好处有两个。首先，它表明Voronkov实现的逆向方法在实践中表现良好，是K的基于自动机的可满足性过程的一种优化即时实现。其次，它可用于给出Voronkov的优化不会破坏过程完整性的更简单的证明。同时我们还将展示逆向方法可以轻松扩展到处理全局公理，并且在这种情况下与自动机方法的对应关系仍然成立。特别地，逆向方法为K关于全局公理的可满足性提供了一个EXPTIME算法。
作者：Franz Baader and Stephan Tobies
论文ID：cs/0412101
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23