In: J. Esparza, C. Lakos (Eds.): Lecture Notes in Computer Science, Vol. 2360: 23rd International Conference on Applications and Theory of Petri Nets, Adelaide, Australia, June 24-30, 2002, pages 273-293. Springer Verlag, June 2002.
Abstract: Coloured Petri Nets (CPNs) are used to model the service provided by an International Standard for the control of multimedia communications over telecommunication networks including the Internet, known as the Capability Exchange Signalling (CES) protocol. The state space of the CPN model includes all of the possible sequences of user observable events, known as the service language, which is a useful baseline against which the protocol can be verified. However, the CES service CPN possesses an infinite state space, due to unbounded communication channels. We parameterize the CPN with the channel capacity, propose and prove a recursive formula for its state space and provide an algorithm for its construction. The algorithm generates the state space for capacity l, from the state space for capacity l-1, providing incremental state space generation rather than generating a new state space for each value of l. The state space is linear in the size of the channel.
Keywords: Multimedia Networks and Protocols; Service Definitions; Parameterization; Coloured Petri Nets; Incremental State Space Algorithms.