Step coverability algorithms for communicating systems (2012)

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.

      • Date: 25-11-2010
      • Journal: Science of Computer Programming
      • Volume: 77
      • Issue: 7-8
      • Pages: 955-967
      • Publisher: Elsevier BV
      • Publication type: Article
      • Bibliographic status: Published

      Keywords: Petri nets, step coverability tree, maximal concurrency, communicating components, determinism


      Professor Maciej Koutny
      CS Director of Research