一种有效的基于LTL和Petri网的模型检测方法

来源 :计算机应用 | 被引量 : 5次 | 上传用户:xujingtony
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包,可以有效地对基于Petri网表示的系统模型进行模型检测。
其他文献
文中提出一种跟踪人脸特征点的方法。使用一系列方向、频率、相位各不相同的Gabor小波 ,对测试序列第一帧中选定的人脸特征点进行小波变化 ,得到对应点的一组小波系数 (Jets) ,并将其作为后续帧的跟踪依据。对含有各种表情的视频序列进行测试 ,试验结果显示该方法是有效的
英语的“形名”结构一般情况下可以对译成汉语的“形名”结构,但有时却需要转译成“名形”结构,是对译还是转译取决于一定的语义条件。其规律是:当“形名”结构的“形”与句中的
针对在删失试验的生存分析中,为了估计不同协变量在组内的相互影响以及一些无法观测的协变量产生的异质影响,在基准危险函数为分段指数的情形下,给出贝叶斯共享异质模型,利用Gibb
对Bayesian网及其概率推理进行了简述,提出并实现了一种以Bayesian理论为基础的查询方法,重点介绍Bayesian网络简化、扩展关系表、功能及概率推理算法。举例说明了系统运行的过程。
通过识别、封装和集成不同种类的关注点来构件系统,从而提高系统的适应性、可维护性和重用性。面向方面编程(AOP)技术是目前较好的分离关注点的编程范式。基于CAR构件系统,提出了AOP的动态聚合模型及其实现。与其他系统的静态聚合方法相比,动态聚合所具有的随时聚合、随时拆卸的特点更加有效的提高了系统的适应性和重用性。
论述游泳运动全能比赛的必要性、可行性,对游泳运动全能比赛的项目设置、竞赛程序、竞赛评分方法做了初步设想,并以模拟成绩公告的方式进行了实验.
通过对RAM和CAM模型的介绍 ,分析了电子政务系统的特点 ,提出了基于代理技术、轻权目录访问协议 (LDAP)、虚拟数据库的电子政务系统。借助LDAP的目录层次 ,建立了电子政务系统的信息定位树状基本结构 ,分析了电子政务系统框架的内容、相关技术和代理功能的内容和处理过程。电子政务系统框架实现了应用的分布式、统一的资源管理、树状的非结构信息向关系数据信息集成。
文中描述了基于直接体绘制的三维数据场交互可视化系统SinoVis的系统设计框架与具体实现。SinoVis是一个纯软件的可视化分析系统,SinoVis绘制的图像精细,可视化参数的设置与调整方便灵活,可以在任意选择的体元分类转移函数下对规模为1283~2563的体数据实现高速交互绘制,在相当广泛的研究与工程领域里有潜在的应用价值。
对LOG算子边缘检测方法的性能进行了分析和评价。针对LOG算子的缺陷,提出了依据图像灰度的一阶导数极大值和二阶导数零穿相结合的边缘检测方法,成功抑制了图像中的大部分噪声;并通过用图像灰度共生矩阵的惯性矩特征值自适应调整高斯空间系数和边缘检测阈值,实现了图像边缘的自动提取。
在客户机/服务器和浏览器/服务器系统模型的基础上,结合多层客户机/服务器系统模型,提出了专用浏览器/服务器系统模型,并给出了一个实例。该模型使得浏览器可通过数据库服务器直接与数据库通信,具有开发成本低、性能更高、安全性更好。最后还给出了专用浏览器/服务器系统模型的其它解决方案。