共查询到18条相似文献,搜索用时 31 毫秒
1.
讨论了以基于前缀封闭集合的Heyting代数的直觉解释的线性μ-演算(IμTL)作为描述“假设-保证”的逻辑基础的问题,提出了一个基于IμTL的“假设-保证”规则.该规则比往常应用线性时序逻辑(LTL)作为规范语言的那些规则具有更好的表达能力,扩展了对形如“always ?”等安全性质的“假设-保证”的范围,具备更一般的“假设-保证”推理能力及对循环推理的支持. 相似文献
2.
模态μ-演算被十分广泛地应用在模型验证技术中.影响模态μ-演算检验复杂度的主要瓶颈来源于规约公式的交换深度.讨论了线性μ-演算交换深度的可判定性以及求解复杂度.证明了线性μ-演算交换深度是可判定的;同时证明了对于长为l的公式判定及求解的复杂度为2O(l logl). 相似文献
3.
随着软硬件系统复杂性的不断提高,各种验证技术被越来越广泛的使用.模型检验技术是一种保证软硬件设计、实现正确性的有效技术.在针对软硬件的模型验证技术中,一般采用时序逻辑作为规约语言.模态μ-演算是模态和时序逻辑中应用较为广泛的一种,它具有语法成分简洁、表达能力强等特点.扩展了Lange和Stirling基于Focus Game的LTL和CTL的公理化方法.提出了一种基于Game理论的μ-演算公式的可满足性的测试方法,该种方法能够将模态μ-演算公式的可满足性问题转化为Focus Game的求解问题.进一步,基于这套Game规则,给出了一个新的关于μ-演算可靠完备的推理系统.同已有的μ-演算公理系统相比,该推理系统相对直观、简洁. 相似文献
4.
《计算机工程与应用》2017,(9):51-56
命题μ-演算局部模型检测算法中,目前最好的算法的时间复杂度与不动点算子交替嵌套深度d呈指数关系。针对命题μ-演算局部模型检测算法的计算过程进行分析,得到迭代计算的中间迭代值间满足的一组偏序关系,然后利用该偏序关系设计了一个局部模型检测算法,算法时间复杂度的指数部分为d/2,大大提高了算法的计算效率。 相似文献
5.
6.
江华 《计算机研究与发展》2010,47(8):1424-1433
在Long, Browne, Jha 和 Marrero等人工作的基础上,详细分析了用Tarski不动点定理计算不动点交替嵌套深度为4的命题μ-演算公式的计算过程,找到了计算中间结果间具有的两组偏序关系,利用这两组偏序关系设计了一个高效的命题μ-演算全局模型检测算法,该算法与Long等人提出的算法有相似的时间复杂度(O((2n+1)\\+{[d/2]+1})相对于O(n\\+[d/2]+1})),但空间复杂度有很大的改进(O(dn)相对于O(n\\+{[d/2]+1})),其中n是变迁系统的状态规模,d是命题μ-演算公式中不动点算子的嵌套深度.算法性能的改进对于命题μ-演算模型检测技术的理论研究与实际推广应用都意义重大. 相似文献
7.
8.
9.
定义了一个命题线性时序逻辑的对偶模型的概念.一个公式f的对偶模型是指f的满足以下条件的两个模型(即状态的w序列):在每个位置上这两个模型对原子命题的赋值都是对偶的.然后,对于确定一个公式f是否有对偶模型的判定问题(记为DM)和在一个Kripke-结构中确定是否存在从两个给定状态出发的对偶模型满足给定公式f的判定问题(记为KDM)的复杂性进行了研究.证明了以下结果:对于只含有F("Future")算子的命题线性时序逻辑,DM和KDM都是NP完全的;而对于以下命题线性时序逻辑,DM和KDM都是PSPACE完全的:含有F,X ("Next")算子的逻辑、含有U("Until")算子的逻辑、含有U,S,X算子的逻辑以及由Wolper给出的含有正规语言算子的逻辑(一般称为扩展时序逻辑,简称ETL). 相似文献
10.
11.
Davide Bresolin Angelo Montanari Guido Sciavicco 《Journal of Automated Reasoning》2007,38(1-3):173-199
Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements
that refer to time intervals. Unfortunately, most such logics turn out to be (highly) undecidable. In order to get decidability,
severe syntactic or semantic restrictions have been imposed to interval-based temporal logics to reduce them to point-based
ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones that
are genuinely interval-based is still largely unexplored. In this paper, we focus our attention on interval logics of temporal
neighborhood. We address the decision problem for the future fragment of Neighborhood Logic (Right Propositional Neighborhood
Logic, RPNL for short), and we positively solve it by showing that the satisfiability problem for RPNL over natural numbers
is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure, and we prove its optimality. 相似文献
12.
13.
14.
SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。 相似文献
15.
16.
17.
首先介绍命题演算的Gentzen型系统G,然后给出一个命题演算的永真推理系统H,最后证明一个命题在G中可证当且仅当它在H中可证,从而G与H是等价的. 相似文献
18.
由一阶逻辑公式得到命题逻辑可满足性问题实例 总被引:2,自引:0,他引:2
命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题. 相似文献