【摘 要】
：
混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对
【机 构】
：
南京大学计算机软件新技术国家重点实验室,南京大学计算机科学与技术系
【基金项目】
：
国家自然科学基金，国家高技术研究发展计划(863计划)，国家重点基础研究发展计划(973计划)，江苏省自然科学基金
论文部分内容阅读
混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机,其对于线性时段性质的满足性能够通过线性规划方法加以检验.为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker.工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息.
其他文献
引入了N-可分效应代数的定义,证明了N-可分效应代数是区间效应代数且N-可分效应代数可嵌入到可分效应代数中.
随着中国保险业的飞速发展，各大保险公司纷纷对原有的业务系统进行更新换代。文章探讨了集中式核心业务系统在风险控制、业务管理、效率提高方面给保险公司带来的有益变化。
文章介绍了某地区无线小区话务分析实时监测系统的设计思想、系统实现,并对系统功能进行了描述.
目的：探讨子痫前期患者甲状腺功能减退的状况,并分析其病情严重程度与母儿结局的关系。方法：选取2015年1月至2017年2月孕晚期孕妇150例,按患子痫前期情况分组,其中轻度子痫前期
由于家庭经营的局限性,参与农业产业化经营的农户往往是分散的,而非组织化的,如果把分散的农户组织起来,如组成专业合作社或专业协会,扩大和提升家庭经营在市场经济中的地位,
现代教育思想观念培养与教师职业技能训练的相互渗透可以通过"单元教学模式"和"四结合"的方法来实现.现代教育思想观念培养与教师职业技能训练两者的相互渗透是目的,"单元教
高校加强诚信建设需要有一个良好的诚信环境.市场经济的发展、高校诚信环境的现状和教育功能的实现与否都要求必须加强诚信环境建设.加强诚信环境建设的措施包括进行校园诚信