论文部分内容阅读
ＬＰＴＬ与自动机之间有着紧密的联系，结合ＬＰＴＬ语义和语法，提出一种从ＬＰＴＬ公式导出Ｂｕｃｈｉ自动机的方法。导出的Ｂｕｃｈｉ自动机所接受的语言准确地表达了ＬＰＴＬ公式所描述的特性。从而把由ＬＰＴＬ公式描述的系统设计规范的验证问题转换成检验Ｂｕｃｈｉ自动机的包含问题。
一种基于时态逻辑的有限状态系统经验证方法
【摘 要】
：
ＬＰＴＬ与自动机之间有着紧密的联系，结合ＬＰＴＬ语义和语法，提出一种从ＬＰＴＬ公式导出Ｂｕｃｈｉ自动机的方法。导出的Ｂｕｃｈｉ自动机所接受的语言准确地表达了ＬＰＴＬ公式所描述的特性。从而把由ＬＰＴＬ公式描述的系统设计规范的验
【出 处】
：
西北工业大学学报
【发表日期】
：
2000年1期
【基金项目】
：
国家自然科学基金!694 73 0 17
其他文献
<正> The endorheic Lake Nam Co, south Eastern Tibetan Plateau, was selected to investigate the interrelationbetween drainage basin processes, especially post-gl
通过数值计算与实验相结合的方法,对凝固组织数值模拟中晶粒接触因素修正系数的已有形式进行了分析、比较.在此基础上,提出了当固相体积分数(fs)大于π/6后采用[1一(fx-π/6)
本文讨论了高维非线性网络模型的搜索法和Ｄｉｊｋｓｔｒａ算法的求解法，并给出了算法的实现步骤．
利用氧同位素作为古高度计重建造山带的古高度是近年发展起来的应用比较广泛的方法。本文通过对青藏高原河水δ^18Ow（SMOW）的空间分布特征分析，表明高原南北δ^18Ow（SMOW）由于水汽
本文研究ＯＵ型Ｍａｒｋｏｖ过程的不变测度、参考测度和弱对偶半群的存在性问题，并得出了不变测度的唯一性。
ＦＣＴ６芯片是一个集成了Ｉｎｔｅｌ８０３１微处理器及一些外围电路的嵌入式微控制器，它的集成度和复杂度高，又有嵌入式ＲＡＭ部件，而且芯片管脚数相对较少，必须要有一定的可测试性设计来简化测试代码，提高故障覆
本文用软代数的素理想集刻划了软代数的每一个同余关系，并给出了软代数的同余理想用素理想集刻划的表达式。
本文中我们对文献［７］中一个主要定理的证明进行了简化，并且给出了格值Ｉ（Ｌ）－ｆｕｚｚｙ拓扑由其水平拓扑确定的条件，从而推广了［７］中定理４．３。
讨论了垂直放置靠火箭推进的水下定向航行器的运动特征，根据其结构特点，并考虑航行器质量变化以及海水水流等的影响，从能量角度出发建立了水下航行器定向运动时的弹道数学模型，最
从当今国际上不同的气候系统模式模拟的全新世大暖期和末次盛冰期我国气候变化量级和复原资料结果的对比，以及从目前气候变化的趋势（包括温室气体、气温、海洋温度、海平面高度