Hierarchy of persistence with respect to the length of action's disability.

arXiv: Logic in Computer Science(2015)

引用 25|浏览8
暂无评分
摘要
The notion of persistence, based on the rule action can disable another is one of the classical notions in concurrency theory. It is also one of the issues discussed in the Petri net theory. We recall two ways of generalization of this notion: the first is action can kill another (called l/l-persistence) and the second action can kill another enabled (called the delayed persistence, or shortly e/l-persistence). Afterwards we introduce a more precise notion, called e/l-k-persistence, in which one action disables another one for no longer than a specified number k of single sequential steps. Then we consider an infinite hie-rarchy of such e/l-k persistencies. We prove that if an action is disabled, and not killed, by another one, it can not be postponed indefinitely. Afterwards, we investigate the set of markings in which two actions are enabled simultaneously, and also the set of reachable markings with that feature. We show that the minimum of the latter is finite and effectively computable. Finally we deal with decision problems about e/l-k persistencies. We show that all the kinds of e/l-k persistencies are decidable with respect to steps, markings and nets.
更多
查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要