Author(s): Kleijn J, Koutny M
Abstract: 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 exhibitnon-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.
Keywords: Petri nets, step coverability tree, maximal concurrency, communicating components, determinism
|
Professor Maciej Koutny
|
|