Modular reachability analysis in fundamental class of multi-agent nets

Multi-agent nets are a variant of Object-oriented Petri nets, and a formal model description language for multi-agent systems. Modular Petri nets have been proposed in order to describe discrete event systems in a modular way. The modular reachability analysis technique for modular Petri nets is powerful, and it would be useful to introduce it into reachability analysis of multi-agent nets. In this paper, we discuss a reachability analysis method for multi-agent nets by using modular Petri nets, and propose a set of transformation rules from a fundamental class of multi-agent nets into modular Petri nets, and show isomorphism of state spaces of the multi-agent nets and them of generated modular Petri nets.