Step coverability algorithms for communicating systems

详细信息	查看全文 | 推荐本文 |

• 作者：Jetty Kleijn^a ; ^{kleijn@liacs.nl} ; Maciej Koutny^b ; ^{maciej.koutny@ncl.ac.uk}
• 关键词：Petri nets ; Step coverability tree ; Maximal concurrency ; Communicating components ; Determinism
• 刊名：Science of Computer Programming
• 出版年：2012
• 期刊代码：108_01676423
• 类别：cp
• 出版时间：1 July, 2012
• 卷：77
• 期：7-8
• 页码：955-967
• 文件大小：366 K

摘要

Coverability (of states) is an important, useful notion for the behavioural analysis of distributed dynamic systems. For systems like Petri nets, the classical Karp-Miller coverability tree construction is the basis for algorithms to decide questions related to the capacity of local states. We consider a modification of this construction which would allow one to deal with dynamic behaviour consisting of concurrent steps rather than single occurrences of transitions. This leads to an action-based extension of the notion of coverability, viewing bandwidth as a resource. However, when certain constraints are imposed on the steps, systems may exhibit non-monotonic behaviour. In those cases, new criteria for the termination of the step coverability tree construction are needed. We investigate a general class of Petri nets modelling systems that consist of components communicating through shared buffers and that operate under a maximally concurrent step semantics. Based on the description of their behaviour, we derive a correctly terminating step coverability tree construction for these Petri nets.