SPACE UPPER BOUND ANALYSIS FOR TRANSFORMATION FROM ELEMENTARY REFERENCE-NET SYSTEM TO LOW-LEVEL P/T NETS

Abstract

Elementary Reference-nett Systems (ERS) is a class of Object-Oriented Petri Nets that follows the nets-within-nets paradigm. It combines theoretical properties as well as numerous practical needs for multi-agent-systems specification. However, it comes with some constraints that limit their expressiveness for automatic verification purposes due to the highly expressive nature of the underlying class of Petri nets. This article presents a set of transformation procedure from ERS to basic Petri nets in order to make verification feasible. It further establishes the space upper bound for the transformation which shows that the state space of the transformed P/T net grows exponentially as the number of object nets increases.