For the most recent entries see the Petri Nets Newsletter.

Modular Verification of Petri Nets Properties: A Structure-Based Approach.

Klai, Kais; Haddad, Serge; Ilie, Jean-Michel

In: Farn Wang (Eds.): Lecture Notes in Computer Science, 3731: Formal Techniques for Networked and Distributed Systems - FORTE 2005: 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005., pages 189-203. Springer-Verlag, October 2005. URL:,.

Abstract: In this paper, we address the modular verification problem for a Petri net obtained by composition of two subnets. At first, we show how to transform an asynchronous composition into a synchronous one where the new subnets are augmented from the original ones by means of linear invariants. Then we introduce a non-constraining rela- tion between subnets based on their behaviour. Whenever this relation is satisfied, standard properties like the liveness and the boundedness and generic properties specified by a linear time logic may be checked by examination of the augmented subnets in isolation. Finally, we give a sufficient condition for this relation which can be detected modularly using an efficient algorithm.

Keywords: Abstraction, modular verification,(de)composition,Petri nets.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography