共查询到20条相似文献,搜索用时 62 毫秒
1.
2.
王富彬 《电脑与微电子技术》2010,(10):8-10,22
分析描述逻辑时态扩展的优缺点,同时结合实际应用需求,将时间当作具体领域加入到描述逻辑中来处理,给出带时态扩展的描述逻辑SHIOQ(T)的形式化描述,并给出SHIOQ(T)中概念、关系和实例的描述形式以及它们的语义解释,从而方便地实现时态知识的表达和推理。 相似文献
3.
4.
5.
时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-工`I'I、中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。 相似文献
6.
基于时态逻辑的硬件设计形式化验证技术--模型检验1 总被引:1,自引:0,他引:1
通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用,同时对布尔函数在计算机内的表示二叉判定图(BDD)进行了进一步地分析,最后给出了一个时态逻辑对硬件设计进行验证的例子. 相似文献
7.
近年来,时态逻辑大量应用于程序验证,采取的途径随使用的时态逻辑的形式和方法的不同而异。本文用自动机理论研究几种时态逻辑(LTL,BTL,POTL)的模型和模型生成子,并讨论用时态逻辑进行程序验证的的重要途径。 相似文献
8.
时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高。将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL。该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言。最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别。通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。 相似文献
9.
10.
间断区间时态逻辑的语义 总被引:1,自引:0,他引:1
区间逻辑不能模拟自然语言中与,或,非时态关系,其公理系统的完备性不易保证。我们建立的间断区间时态知脚注可以克服区间逻辑的上述缺点,本文给出了间断区间逻辑的语法,语义及公理,即描述了间断区间时态逻辑的语义。 相似文献
11.
The modal μ-calculus is a very expressive temporal logic. In particular, logics such as LTL, CTL and CTL* can be translated into the modal μ-calculus, although existing translations of LTL and CTL* are at least exponential in size. We show that an existing simple first-order extension of the modal μ-calculus allows for a linear translation from LTL. Furthermore, we show that solving the translated formulae is as efficient as the best known methods to solve LTL formulae directly. 相似文献
12.
The Expressive Power of Temporal Logic of Actions 总被引:1,自引:0,他引:1
13.
For a dynamic logic L we study dynamic logics Ln for which programs allowed in formulas cannot use more than n variables. We prove that there exists a structure A of a finite signature such that for a wide class of dynamic logics L and for every natural number n the logic Ln+1 is more expressive over A than Ln. This result is based on a construction of some canonical form for the formulas of Ln over a free one-generated groupoid. 相似文献
14.
Ågotnes Thomas Alechina Natasha Galimullin Rustam 《Journal of Logic, Language and Information》2022,31(2):141-166
Journal of Logic, Language and Information - Public announcement logic (PAL) is an extension of epistemic logic with dynamic operators that model the effects of all agents simultaneously and... 相似文献
15.
16.
Resolution for Temporal Logics of Knowledge 总被引:6,自引:0,他引:6
17.
18.
Catuscia Palamidessi Mogens Nielsen Frank D. Valencia 《Electronic Notes in Theoretical Computer Science》2002,68(2)
The tcc paradigm is a formalism for timed concurrent constraint programming. Several tcc languages differing in their way of expressing infinite behavior have been proposed in the literature. In this work we study the expressive power of some of these languages. In particular, we show that: (1) recursive procedures with parameters can be encoded into parameterless recursive procedures with dynamic scoping, and viceversa. (2) replication can be encoded into parameterless recursive procedures with static scoping, and viceversa. (3) the languages from (1) are strictly more expressive than the languages from (2). Furthermore, we show that behavioral equivalence is undecidable for the languages from (1), but decidable for the languages from (2). The undecidability result holds even if the process variables take values from a fixed finite domain.(Joint work with Mogens Nielsen and Frank D. Valencia) 相似文献
19.
We consider extensions of first order logic (FO) and fixed point logic (FP) by means of generalized quantifiers in the sense of Lindström. We show that adding a finite set of such quantifiers to FP fails to capture PTIME, even over a fixed signature, strengthening earlier results. We also prove a stronger version of this result for PSPACE, which enables us to establish that PSPACE ≠ FO on any infinite class of ordered structures, a weak version of the ordered conjecture formulated by Ph. G. Kolaitis and M. Y. Vardi (Fixpoint logic vs. infinitary logic in finite-model theory, in "Proceedings, 7th IEEE Symposium on Logic in Computer Science, 1992," pp. 46-57). These results are obtained by defining a notion of element type for bounded variable logics with finitely many generalized quantifiers. Using these, we characterize the classes of finite structures over which the infinitary logic Lω∞ω extended by a finite aw set of generalized quantifiers Q is no more expressive than first order logic extended by the quantifiers in Q. 相似文献
20.
Ian J. Hayes 《Formal Aspects of Computing》1998,10(2):187-192
By abstracting away from a particular specification language and considering a ‘specification’ to be just a set of implementations,
one can define a partial order on specification languages that reflects their expressive power. In addition, one can show
that there is no universal specification language that can express all such ‘specifications’.
Received August 1996 / Accepted in revised form April 1998 相似文献