Nested Petri Nets — a Formalism for Specification and Verification of Multi-Agent Distributed Systems

Article type: Research Article

Authors: Lomazova, Irina A.

Affiliations: Center for Artificial Intelligence, Program Systems Institute of Russian Academy of Science, Pereslavl-Zalessky, 152140, Russia. [email protected]

Note: [] Address for correspondence: Center for Artificial Intelligence, Program Systems Institute of Russian Academy of Science, Pereslavl-Zalessky, 152140, Russia

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.

Keywords: hierarchical multi-agent systems, nested Petri nets, well-structured transition systems, decidibility

DOI: 10.3233/FI-2000-43123410

Journal: Fundamenta Informaticae, vol. 43, no. 1-4, pp. 195-214, 2000