Paper Info
Title
An algorithm for direct construction of complete merged processes
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-21834-7_6
Petri Nets
Keywords
Field
DocType
direct construction,state space explosion,complete merged process,challenging problem,practical model checking,merged process,efficient model checking,traditional unfoldings,condense representation,model checking,sat
Discrete mathematics,Model checking,Petri net,Computer science,Concurrency,Algorithm,Prefix,Theoretical computer science,State space,Branching process
Conference
Volume
ISSN
Citations 
6709
0302-9743
4
PageRank 
References 
Authors
0.45
19
2
Name
Order
Citations
PageRank
Victor Khomenko128620.67
Andrey Mokhov213626.57