TY - GEN
T1 - A petri net reduction algorithm for protocol analysis
AU - Ramamoorthy, C. V.
AU - Yaw, Y.
AU - Tsai, W. T.
N1 - Publisher Copyright:
© 1986 ACM.
PY - 1986/9/30
Y1 - 1986/9/30
N2 - Petri net is a powerful model for analyzing communication protocols because they share many common properties. Currently, protocol analysis suffers the state explosion problem especially for error-recoverable protocols and multiparty protocols. Protocol synthesis relieves this problem by generating new and complicated protocols from simple subsets of the protocol models. Reduction analysis provides theoretical ground for correct synthesis or expansion. Thus, reduction is a very important research area. In this paper, we present a general Petri net reduction algorithm that reduces the number of states while preserving all desirable and undesirable properties. To the best of our knowledge, this is the first general Petri net reduction algorithm for protocol analysis. We first present and extend Dong's [DON 83] definition of WBMs to include more subnets as WBMs. To render the reductions automated, a new concept of simple well-behaved modules (SWMs) is introduced. Recursively performing reductions of SWBMs, complicated WBMs can be reduced. A main program is written to implement this recursive procedure. The problem is then reduced to finding conditions for SWBMs. We do this by progressing from simpler SWBMs to more complicated ones, i.e., from single-arc ones to multi-arcs ones. Finally, we demonstrate the usefulness of this algorithm by applying it to the state exploration in protocol synthesis. Other applications such as error detection, performance evaluation, and software engineering will be discussed in future.
AB - Petri net is a powerful model for analyzing communication protocols because they share many common properties. Currently, protocol analysis suffers the state explosion problem especially for error-recoverable protocols and multiparty protocols. Protocol synthesis relieves this problem by generating new and complicated protocols from simple subsets of the protocol models. Reduction analysis provides theoretical ground for correct synthesis or expansion. Thus, reduction is a very important research area. In this paper, we present a general Petri net reduction algorithm that reduces the number of states while preserving all desirable and undesirable properties. To the best of our knowledge, this is the first general Petri net reduction algorithm for protocol analysis. We first present and extend Dong's [DON 83] definition of WBMs to include more subnets as WBMs. To render the reductions automated, a new concept of simple well-behaved modules (SWMs) is introduced. Recursively performing reductions of SWBMs, complicated WBMs can be reduced. A main program is written to implement this recursive procedure. The problem is then reduced to finding conditions for SWBMs. We do this by progressing from simpler SWBMs to more complicated ones, i.e., from single-arc ones to multi-arcs ones. Finally, we demonstrate the usefulness of this algorithm by applying it to the state exploration in protocol synthesis. Other applications such as error detection, performance evaluation, and software engineering will be discussed in future.
UR - https://www.scopus.com/pages/publications/84987255018
U2 - 10.1145/18172.18191
DO - 10.1145/18172.18191
M3 - 会议稿件
AN - SCOPUS:84987255018
T3 - Proceedings of the ACM SIGCOMM Conference on Communications Architectures and Protocols, SIGCOMM 1986
SP - 157
EP - 166
BT - Proceedings of the ACM SIGCOMM Conference on Communications Architectures and Protocols, SIGCOMM 1986
A2 - Kosinsky, Walter
A2 - Garcia-Luna, J. Joaquin
A2 - Kuo, Franklin F.
PB - Association for Computing Machinery
T2 - 1986 ACM SIGCOMM Conference on Communications Architectures and Protocols, SIGCOMM 1986
Y2 - 5 August 1986 through 7 August 1986
ER -