ePrints

Step coverability algorithms for communicating systems

Lookup NU author(s): Professor Maciej KoutnyORCiD

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.

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.

Publication metadata

Author(s): Kleijn J, Koutny M

Publication type: Article

Publication status: Published

Journal: Science of Computer Programming

Year: 2012

Volume: 77

Issue: 7-8

Pages: 955-967

Print publication date: 25/11/2010

ISSN (print): 0167-6423

ISSN (electronic): 1872-7964

Publisher: Elsevier BV

URL: http://dx.doi.org/10.1016/j.scico.2010.11.003

DOI: 10.1016/j.scico.2010.11.003

Altmetrics

Share