Abstract: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 behavioral influence of invisible action τ.This leads to behavior inconsistency between choreography and the generated peers.This paper proposes a projection approach based on Petri nets,which allows us to 1) generate the peers defined by interaction Petri nets with τ through action projection from a choreography defined by an interaction Petri net,2) develop four types of tau deletion rules to selectively delete τ of interaction Petri nets,and 3) specify the behavior consistency between choreography and the generated peers to check whether two Petri nets meet the weak simulation.Moreover,the correctness of these four types of tau deletion rules is proved.Experimental results show that the projection approach can ensure the behavior consistency between choreography and peers.