A Choreography Projecting Method Based On Weak Bisimulation

That peers are generated by projection from Choreographies is known as the first step in checking choreographies' realizability.However,the projection approaches proposed by the existing literature have not considered the influence of invisible action? on behavior.This leads to behavior inconsistency between choreography and the generated peers.In this paper,we propose a projection approach based on Petri nets,which allow us to 1)the peers with redundant invisible action ? defined by role Petri nets are generated by action projection from a choreography defined by an interaction Petri net,2)four ? deletion rules are proposed to selectively delete ? of the role Petri nets,3)The behavior consistency between the choreography and the generated peers is specified to check whether two Petri nets meet the weak simulation.Moreover,the correctness of these four ? delete rules is proved.Experiments show that the projection approach can ensure the behavior consistency between choreography and peers.In this paper,we mainly use the method based on weak bisimulation to ensure the consistency between the peers and the participants.For this purpose,the main work of this paper is as follows:First,we propose a mapping method and define action mapping.Action mapping is to map the actions that are unrelated to the participants(Peer)to an invisible action ?.Second,put forward the ? deletion rules,the rules of a total of four.Based on the weak bisimulation,the ? operation in the Petri structure is deleted,and the corresponding Petri network is obtained.Third,to verify the correctness of the ? deletion rule,the standard is based on the weak bisimulation relationship between the source role Petri net and the target role Petri network behavior comparison.Fourth,select the experiment in the five papers,and compare them with the method of this paper.The experimental results suggest that the proposed method can't fully guarantee the consistency between the choreography and the participants in the weak bisimulation relationship,but the proposed method can.In a word,this paper proposes a method of layout mapping to ensure the consistency between the choreography and the peers.