Datalog LITE: a deductive query language with linear time model checking
Datalog LITE: a deductive query language with linear time model checking
复制标题
DOI：
10.1145/504077.504079
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
G. Gottlob;E. Grädel;H. Veith
中科院分区：
文献类型：
--
作者：
G. Gottlob;E. Grädel;H. Veith
我们提出Datalog Lite，这是一种具有线性时间模型检查算法的新的演绎查询语言，即线性时间数据复杂性和程序复杂性。统治物体中的通用量化。尽管有线性时间评估，但Datalog Lite具有高度表达性：它包括流行的模态和临时逻辑，例如CTL或The实际上，这些形式上的μ-钙符号为datalog lite的片段。提到的逻辑是以统一的方式获得的。结果是通过不可表达的证据来完成的，以表明分层数据核的线性时间片段的表达能力过于有限。
We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable occurrences and a limited form of universal quantification in rule bodies.Despite linear-time evaluation, Datalog LITE is highly expressive: It encompasses popular modal and temporal logics such as CTL or the alternation-free μ-calculus. In fact, these formalisms have natural presentations as fragments of Datalog LITE. Further, Datalog LITE is equivalent to the alternation-free portion of guarded fixed-point logic. Consequently, linear-time model checking algorithms for all mentioned logics are obtained in a unified way.The results are complemented by inexpressibility proofs to the effect that linear-time fragments of stratified Datalog have too limited expressive power.