Token Trail Semantics II - Petri Nets And Their Net Language

There are various semantics for Petri nets. Some semantics can express concurrency well, others are good at modelling conflicts. Yet, every semantics has its drawbacks. State graphs explode in size when there is concurrency. Sequential and partial languages explode in size if there is conflict. In our previous paper on token trail semantics, we introduced the concept of the net language of a marked Petri net. The net language is a set of labelled nets so that we can specify both conflict and concurrency very naturally. We proved that the token trail semantics faithfully covers state graphs, sequential languages, and partial languages. In this paper, we show token trail semantics covers synchronous net morphisms and prove the net language of a Petri net includes all its finite unfoldings. Furthermore, we show that a Petri net simulates the state-transition behaviour of all labelled nets of its net language and prove the step language of a Petri net is the union of the step languages of all labelled nets of its net language. Finally, we present an algorithm and an implementation deciding the net language inclusion problem.