论文部分内容阅读
为了提高基于Petri网表示的嵌入式模型（PRES＋）验证的效率，对模型进行了保性变换，给出了一组关于PRES＋模型的化简规则，这些化简规则在原模型和简化模型之间保持完全等价关系。对两个系统模型的化简结果进一步说明了这些化简规则的有效性。
基于Petri网表示的嵌入式系统模型化简规则
【摘 要】
：
为了提高基于Petri网表示的嵌入式模型（PRES＋）验证的效率，对模型进行了保性变换，给出了一组关于PRES＋模型的化简规则，这些化简规则在原模型和简化模型之间保持完全等价关系。对两个
【机 构】
：
山东建筑大学计算机学院,中国科学院软件研究所计算机科学国家重点实验室
【出 处】
：
计算机科学与探索
【发表日期】
：
2008年6期
【基金项目】
：
the National Natural Science Foundation of China under Grant No.60573012,No.60721061（国家自然科学基金）,the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200（国家重点基础研究发展规划（973
其他文献
目的观察阻塞性睡眠呼吸暂停低通气综合征（OSAHS）病人解除上呼吸道梗阻的手术治疗对肺动脉压力（pulmonary artery pressure，PAP）和血肾上腺髓质素（adrenomedullin，ADM）的变化的影响。
作为个性化服务技术的核心,用户模型的质量关系到个性化服务的质量。目前的用户模型大多只考虑用户的显式信息或隐式信息,很少同时考虑两者,使得检索质量不如人意。提出了一
在国家自然科学基金项目资助下，2011年，国内学者又有涉及几何处理、建模、绘制、图像视频等方向的多项研究成果在ACM SIGGRAPH上发表。
干预决策是数据挖掘领域关注的重要问题，致力于评价干预措施对干预目标的影响或发现满足干预目标的最优干预措施，而朴素干预规则模型简单，无法精确表达干预知识，且效率较差。在模
随着质谱技术的迅猛发展，通过色谱质谱联用（liquid chromatography mass spectrometry，LCMS）技术进行化合物鉴定成为近年来的研究热点。针对化合物LC．MS鉴定过程中便捷性和效率问
目的探讨利用等离子双极射频治疗小儿阻塞性睡眠呼吸暂停低通气综合征（OSAHS）的临床疗效。方法4-13岁OSAHS患儿56例,全麻下利用等离子双极射频切除扁桃体和（或）经鼻内镜下利用等
通过结合拟阵理论,建立了覆盖粗糙集的横贯拟阵结构;在此结构下,建立了覆盖与正规拟阵间的联系,揭示了覆盖变化与相应的横贯拟阵变化的关系;进一步给出了由任一拟阵导出覆盖
列的连接策略优化是列存储数据查询中的重要问题。现有的列存储系统中，列的连接存在策略单一，缺少优化处理，无法满足复杂查询等缺陷。针对这些问题，提出一种连接策略选择方法。该