Courier-Protocol
The Courier-protocol describes a unidirectional communication protocol.
A Petri-net specification of the protocol has been first published in [1].
In [2] the protocol is used as an example to show the generation of hierarchical
automata networks from Petri-net specifications.
APNN-Description
The model is described as a hierarchical net with 4 subnets. Subnets communicate
via shared transitions. The hierarchical description corresponds to a partition
of the set of places such that each subnet specifies one automaton/component
of the net. The transitions visible in the upper level are all synchronized
transitions, the remaining transitions inside the subnets are local. Transitions
rates in the model are identical to the rates given in [1].
The state space size of the model is scalable by the window size which
corresponds to the number of tokens in the initial marking of the
places p14 of subnet sender_transport_layer. The size of the state space
for different window sizes can be found in [2].
Automata-Description
The automata description of the example includes the matrices for a model
with window size 3 which results in a CTMC with 419,400 reachable states
and 2,281,620 transitions.
- Matrices of the flat automata network
with a potential state space including 8,593,200 states.
- Matrices of the hierarchical
automata network with 13 states in the upper level and a potential state
space that is identical to the reachable state space.
References
- C. M. Woodside, Y. Li: Performance Petri net analysis of communications
protocol software by delay equivalent aggregation. Proc. PNPM'91, IEEE CS-Press,
1991, pp. 64-73.
- P. Buchholz: Hierarchical structuring of superposed GSPNs. IEEE Trans.
on Software Engineering 25, 1999, pp. 166-181.