共享合成Petri 网系统的活性保持性

讨论了能对资源共享问题进行建模的共享合成操作.重点研究共享合成Petri网系统的活性保持性,同时还讨论了在共享合成过程中系统的并发行为关系即并发语言关系.给出相应的语言关系式,它可用于判定合成系统的活性.进一步,给出了判定合成系统有活性的充分必要条件.最后,提出了合成系统保持子系统活性的条件.     

结合搜索空间划分和抽象进行LTL模型检测

在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.     

同步合成Petri 网系统可回复性的保持性

着重研究同步合成操作中可回复性的保持性.讨论了在同步合成操作中系统间动态、并发的行为关系,即语言关系.提出一种基于最小可回复路径及它们并发合成的方法.进一步,给出了一个合成系统有可回复性的充分必要条件.此外,提出了在同步合成操作中有可回复性的条件.最后给出一些例子来说明所提出的方法在建模和分析大系统时的有效性.     

Petri网系统合成操作的活性保持性研究

合成操作是Petri网系统建模中一种重要的自底向上建模方法,而在Petri网系统的合成过程中,保性性质是一个重要的研究问题.本文综述了我们对Petri网系统两种合成操作(共享合成、同步合成)活性保持性的研究工作.与以往研究不同,侧重从并发语言的角度讨论.定义了相应合成操作的路径并发合成运算,以此建立两种合成操作Petri网系统的并发语言关系式.这些语言关系式可用于判定相应合成操作Petri网系统的活性与无死锁性,同时给出合成的Petri网系统活性与无死锁性的充要条件.最后分别给出条件使得合成的Petri网系统有活性保持性质.