An Algorithm for Direct Construction of Complete Merged Processes

  1. Lookup NU author(s)
  2. Dr Victor Khomenko
  3. Dr Andrey Mokhov
Author(s)Khomenko V, Mokhov A
Editor(s)Kristensen, L.M., Petrucci, L.
Publication type Conference Proceedings (inc. Abstract)
Conference Name32nd International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency (PETRI NETS)
Conference LocationNewcastle upon Tyne, UK
Year of Conference2011
Date20-24 June 2011
Volume6709
Pages89-108
Series TitleLecture Notes in Computer Science
ISBN9783642218347
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
Merged process is a recently proposed condense representation of a Petri net’s behaviour similar to a branching process (unfolding), which copes well not only with concurrency, but also with other sources of state space explosion like sequences of choices. They are by orders of magnitude more condense than traditional unfoldings, and yet can be used for efficient model checking.However, constructing complete merged processes is difficult, and the only known algorithm is based on building a (potentially much larger) complete unfolding prefix of a Petri net, whose nodes are then merged. Obviously, this significantly reduces their appeal as a representation that can be used for practical model checking.In this paper we develop an algorithm that avoids constructing the intermediate unfolding prefix, and builds a complete merged process directly. In particular, a challenging problem of truncating a merged process is solved.
PublisherSpringer Verlag
URLhttp://dx.doi.org/10.1007/978-3-642-21834-7_6
DOI10.1007/978-3-642-21834-7_6
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item