Translation of Nested Petri Nets into Classical Petri Nets for Unfoldings Verification
| Autor: | V. O. Ermakova, I. A. Lomazova |
|---|---|
| Jazyk: | English<br />Russian |
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | Труды Института системного программирования РАН, Vol 28, Iss 4, Pp 115-136 (2018) |
| Druh dokumentu: | article |
| ISSN: | 2079-8156 2220-6426 |
| DOI: | 10.15514/ISPRAS-2016-28(4)-7 |
| Popis: | Nested Petri nets (NP-nets) have proved to be one of the convenient formalisms for distributed multi-agent systems modeling and analysis. It allows representing multi-agent systems structure in a natural way, since tokens in the system net are Petri nets themselves, and have their own behavior. Multi-agent systems are highly concurrent. Verification of such systems with model checking method causes serious difficulties arising from the huge growth of the number of system intermediate states (state-space explosion problem). To solve this problem an approach based on unfolding system behavior was proposed in the literature. Earlier in [4] the applicability of unfolding for nested Petri nets verification was studied, and the method for constructing unfolding for safe conservative nested Petri nets was proposed. In this work we propose another method for constructing safe conservative nested Petri nets unfoldings, which is based on translation of such nets into classical Petri nets and applying standard method for unfolding construction to them. We discuss also the comparative merits of the two approaches. Key words: multi-agent systems; verification; Petri nets; nested Petri nets; unfoldings. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|