共查询到20条相似文献,搜索用时 327 毫秒
1.
为讨论可能的计算树逻辑(PoCTL)与计算树逻辑(CTL)的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别. 相似文献
2.
《华中科技大学学报(自然科学版)》2010,(8)
针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例. 相似文献
3.
李文翔 《安庆师范学院学报(自然科学版)》2018,24(3):65-68
根据温控系统的特征以及需求说明,利用π-演算构建了该系统动态行为的交互模型,依据π-演算的反应规则仿真描述模型的行为交互过程,使用μ-演算和移动工作平台(MWB)工具分析和验证了该交互模型具有温度控制和阈值修改功能,从形式上证明了温控系统的需求说明及其π-演算模型的一致性。结果表明,π-演算能够清楚地描述和分析并发系统的行为交互,而μ-演算可以证明模型的有效性和正确性。 相似文献
4.
形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径.介绍了形式化验证方法之一,模型检验的理论基础和实现方法.介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法.最后使用SMV工具在一个CISC处理器的存储管理单元(MMU)上应用了模型检验,验证了模型检验在模块级验证中的可行性. 相似文献
5.
PPTL模型检测器实现的一个关键技术 总被引:2,自引:1,他引:1
针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测. 相似文献
6.
Jacobi猜想的逻辑化约 总被引:1,自引:0,他引:1
田卫东 《北京师范大学学报(自然科学版)》1988,(3)
提出有关Jacobi猜想的两个命题:A.若Janobi猜想在有理数域Q上成立,则Jacobi猜想在代数域Q上成立.B.对每个正整数对(n,d),存在正整数f(n,d)使得:对每个素数p>f(n,d)及每个特征数p的域K,若多项式映射F:K~n→K~n适合degF≤d且detJ(F)=1,则F可逆.然后用模型论方法证明了定理:“命题A与B成立”等价干“Jacobi猜想对一切特征数0的域成立”. 相似文献
7.
张秀玉 《四川大学学报(自然科学版)》2015,52(6):1277-1284
由于服务聚合要实现异构多态交互过程,必然对安全访问控制模型的性能提出较高的要求.为满足服务聚合的访问控制需求,本文提出了一种异构服务聚合协同访问控制算法ACAHSP.首先,本文剖析了服务聚合中访问的动态情景要素构成,从多维度定义了构成情景的不同要素;然后,提出了基于动态情景状态的状态演算和规则演算的机制,并给出了动态情景机约束下在服务聚合模型ACAHSP;其次,基于CP ABE算法提出了ACAHSP访问控制模型的安全验证算法,强有力的保证了ACAHSP模型在服务聚合中访问控制机制状态机转换、数据交互的安全性;最后,结合案例进行应用验证,并与已有模型进行对比. 相似文献
8.
张会凌 《甘肃联合大学学报(自然科学版)》2006,20(1):25-27,34
在文[1]的基础上,给出了命题逻辑中任一命题公式的真值表的生成算法与命题公式类型的判定算法,实现了利用计算机对有限多个命题公式的真值表的直接计算和输出,以及对一个命题公式是重言式、矛盾式或可满足式的机械判定. 相似文献
9.
关于复合求积公式余项的研究 总被引:4,自引:0,他引:4
借助积分相关理论,给出了数值积分中复合梯形公式和复合Simpson求积公式余项误差事后估计式的严格证明及其余项表达式中的导数因子f″(ηn),f″(η2n),f(4)(ηn)和f(4)(η2n)在n充分大时的变化情况.为处理求积公式余项关系式提供了新的方法. 相似文献
10.
陈彤 《西安工程科技学院学报》2006,20(5):603-606
利用模型检验技术来验证具有“X” (未知)值的属性.给出了三值(真、假、未知)逻辑公式的模型检验算法,此算法与二值逻辑模型检验算法相比,并没有增加时间复杂度.通过实例说明三值逻辑模型检验算法的应用. 相似文献
11.
对于给定的权函数 dμ(x) ,若存在 n次首 1多项式 P*n (x) (称为 s-正交多项式 )使下列积分F(s,μ) =∫R[Pn(x) ]2 s+ 2 dμ(x)达到极小 ,Pn(x) =xn +an- 1 xn- 1 +… +a1 x +a0 ,则以多项式 P*n (x)的 n个不同零点 x1 >x2 >… >xn- 1 >xn 作为节点的下列求积公式 (称为 Gauss-Turán求积公式 )∫Rf (x) dμ(x) =∑2 sj=0 ∑nk=1Ajkf ( j) (xk) +E2 s,n(f ) .具有代数精确度 2 (s+1 ) n -1 .但我们对 F (s,μ)所知不多 .Milovanovic′在他最近的一篇文章里提出计算 F(s,μ)的值 .本文主要解决了若干权函数下的上述极小值问题 相似文献
12.
《海南大学学报(自然科学版)》2017,(1)
对任意正整数n,通过对Smarandache可乘函数f(n),因子积数列Pd(n)及除数函数d(n)进行构造,并利用初等方法及素数分布的性质对建立的∑n≤x(f(P_d(n))-1/2d(n)P(n))~β的混合均值问题进行研究,给出了一个较强的渐近公式. 相似文献
13.
采用LSC(live sequence chart)描述基于场景的需求规格说明,根据设计模型必须满足需求规格说明的一致性原理,针对安全性、可达性、活性等性质,设计3种用于自动生成和抽取性质的覆盖准则,并根据准则从LSC需求规格说明中抽取与设计模型相关的性质.抽取的结果可用于自动化验证,为验证需求模型与设计模型的一致性提供保障. 相似文献
14.
文献[1]论证n阶群同构类的个数在1000以内的存在性。文章给出群同构类Balass计数公式运算的算法,用计算机代数语言Matlab加以实现,进而将群同构类的个数推广到3000。即设f(n)为n阶群同构类的个数,证明方程f(n)=k,(1≤k≤3000)解的存在性。 相似文献
15.
《云南大学学报(自然科学版)》2016,(2)
为了对普遍存在于电子系统和通信系统中的有源噪声进行控制,提出了一种基于快速阵列算法实现的IIR数字滤波器.在对基于传统RLS算法实现的IIR滤波器深入分析的基础上,通过把次级通道的传递函数与回归向量ψf(n)结合起来,并从回归向量ψf(n)的数据结构出发,把回归向量分解为滤波器的先前输出采样ψ1f(n)和参考信号采样ψ2f(n);通过保范映射和内积矩阵形式,最终得到用于滤波器系数更新的阵列形式;同时还比较了2种算法的计算复杂度.仿真结果表明,提出的快速阵列算法不仅降低了计算复杂度,而且对有源噪声信号的相消控制,其收敛速度相对于基于传统RLS算法的收敛速度快大约46%. 相似文献
16.
一种基于模型检验的类测试用例生成方法 总被引:1,自引:0,他引:1
提出一种新的自动生成类测试用例的方法.使用符号执行从类源代码抽取对象的状态和行为,以一个四元组抽象描述类,并转化成等价的Kripke结构.使用CTL公式描述测试覆盖标准,然后把这组CTL公式和描述类状态行为的Kripke结构输入模型检验工具,并利用模型检验工具自动生成相应的证据路径,最后将路径转化成满足相应覆盖标准的类测试用例.该方法直接从源代码生成测试用例,并使用贪心法约减冗余用例以降低测试成本.实验表明该方法生成的测试用例具有较高的覆盖率. 相似文献
17.
王雅玲 《北京工商大学学报(自然科学版)》2002,20(2):56-58
考虑一种特殊的线性分式 f( x) =x- 1x+ d,证明适当选择常数 d,可以得到自迭代周期等于n( n≥ 3)的线性分式 ;并给出矩阵形式的等价命题 ,通过矩阵运算 ,利用复数性质 ,得到 d的表达式 . 相似文献
18.
《山东理工大学学报:自然科学版》2021,(4)
针对物联网服务建模和验证问题,用π-演算理论对物联网服务和环境实体进行动态交互行为建模,并引入μ-演算刻画物联网服务能力,将其描述为物联网服务和环境实体动态交互行为的执行序列。针对特定的应用场景,使用π-演算定义了物联网服务和环境实体,利用μ-演算对物联网服务能力进行建模,使用检测工具MWB验证了模型的安全性、活性和时间约束三个性质,为物联网服务建模和验证提供了参考。 相似文献
19.
《山东大学学报(理学版)》2016,(2)
在模态逻辑S4中通过有限模型建立了模态公式的(n)真度理论,研究了模态逻辑S4中命题的(n)真度的性质。提出了模态公式间的(n)相似度理论,并由此在全体公式集中,建立了(n)伪距离,得出了(n)模态逻辑S4的度量空间,该空间以经典逻辑度量空间为子空间,提出了一种模态逻辑S4中近似推理的框架。 相似文献
20.
针对标准小脑模型关联控制器(CMAC)存在的问题,研究了一种单输入单输出(SISO)的CMAC算法.SISO CAMC采用直接地址映射,以输入v的量化值为地址,建立起输入v与权重w的关系,并通过对输入v进行归一化,增强网络的泛化能力.另外,学习采用随机样本,具有学习简单、收敛速度快、函数逼近精度高等特点,可以在单片机上实现.最后,理论证明和仿真试验,验证了该算法的有效性. 相似文献