Abstract
Nested Petri nets is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. Decidability of some crucial for verification problems shows that, in spite of their ”unflat” structure, nested Petri nets maintain significant properties of ordinary Petri nets. A comparison with some other Petri net models is given. The formalism allows generalization to a recursive case, when a nested Petri net may generate its own copy as its element. Two simple examples illustrate the approach.